Update to lean version v4.15.0

Duper/DUnif/Bindings.lean

@@ -55,14 +55,14 @@ def iteration (F : Expr) (p : UnifProblem) (eq : UnifEq) (funcArgOnly : Bool) :
         let mut lctx ← getLCtx
         for j in List.range i do
           let yty_ty ← Meta.mkFreshLevelMVar
-          let yty ← withReader (fun ctx : Meta.Context => { ctx with lctx := lctx }) do
+          let yty ← Meta.withLCtx' lctx do
             Meta.mkFreshExprMVar (mkSort yty_ty)
           let fvarId ← mkFreshFVarId
           lctx := lctx.mkLocalDecl fvarId s!"iter{i}.{j}".toName yty .default
           let fvar := mkFVar fvarId
           ys := ys.push fvar
         -- Make Gᵢs
-        let lastExpr ← withReader (fun ctx : Meta.Context => { ctx with lctx := lctx }) do
+        let lastExpr ← Meta.withLCtx' lctx do
           let (xys, _, _) ← Meta.forallMetaTelescopeReducing αi
           let body := mkAppN xi xys
           Meta.mkLambdaFVars ys body

Duper/MClause.lean

@@ -27,7 +27,7 @@ def appendLits (c : MClause) (lits : Array Lit) : MClause :=
   ⟨c.lits.append lits⟩
 
 def eraseLit (c : MClause) (idx : Nat) : MClause :=
-  ⟨c.lits.eraseIdx idx⟩
+  ⟨c.lits.eraseIdxIfInBounds idx⟩
 
 def replaceLit? (c : MClause) (idx : Nat) (l : Lit) : Option MClause :=
   if idx >= c.lits.size then
@@ -45,7 +45,7 @@ def mapWithPos (f : Expr → Expr × Array ExprPos) (c : MClause) : MClause × A
   let mapres := c.lits.map (fun l => l.mapWithPos f)
   let c' := ⟨mapres.map (fun x => x.fst)⟩
   let cps := mapres.mapIdx (fun i x => x.snd.map (fun pos => {pos with lit := i}))
-  (c', cps.concatMap id)
+  (c', cps.flatMap id)
 
 def mapMWithPos [Monad m] [MonadLiftT MetaM m] (f : Expr → m (Expr × Array ExprPos)) (c : MClause) : m (MClause × Array ClausePos) := do
   let mapres ← c.lits.mapM (fun l => l.mapMWithPos f)
@@ -112,7 +112,7 @@ def abstractAtPos! (c : MClause) (pos : ClausePos) : MetaM MClause := do
 
 def append (c : MClause) (d : MClause) : MClause := ⟨c.lits.append d.lits⟩
 
-def eraseIdx (i : Nat) (c : MClause) : MClause := ⟨c.lits.eraseIdx i⟩
+def eraseIdx (i : Nat) (c : MClause) : MClause := ⟨c.lits.eraseIdxIfInBounds i⟩
 
 def isTrivial (c : MClause) : Bool := Id.run do
   -- TODO: Also check if it contains the same literal positively and negatively?

Duper/Rules/Clausification.lean

@@ -458,7 +458,7 @@ def clausificationStep : MSimpRule := fun c => do
             let r ← orCases (parentLits.map Lit.toExpr) caseProofs
             let r ← Meta.mkLambdaFVars xs $ mkApp r appliedPremise
             return r
-      let newClause := ⟨c.lits.eraseIdx i ++ d⟩
+      let newClause := ⟨c.lits.eraseIdxIfInBounds i ++ d⟩
       trace[duper.rule.clausification] "Yielding newClause: {newClause.lits}"
       let newResult ← yieldClause newClause "clausification" mkProof tr
       resultClauses := resultClauses.push newResult

Duper/Util/Misc.lean

@@ -11,7 +11,7 @@ def List.subsequences (xs : List α) :=
 -- replace `whnf e` with `e`.
 private partial def instantiateForallAux (ps : Array Expr) (i : Nat) (e : Expr) : MetaM Expr := do
   if h : i < ps.size then
-    let p := ps.get ⟨i, h⟩
+    let p := ps.get i h
     match e with
     | Expr.forallE _ _ b _ => instantiateForallAux ps (i+1) (b.instantiate1 p)
     | _                => throwError "invalid instantiateForallNoReducing, too many parameters"
@@ -20,7 +20,7 @@ private partial def instantiateForallAux (ps : Array Expr) (i : Nat) (e : Expr)
 
 private partial def instantiateForallAuxNoError (ps : Array Expr) (i : Nat) (e : Expr) : Expr :=
   if h : i < ps.size then
-    let p := ps.get ⟨i, h⟩
+    let p := ps.get i h
     match e with
     | Expr.forallE _ _ b _ => instantiateForallAuxNoError ps (i+1) (b.instantiate1 p)
     | _ => panic! "Called instantiateForallAuxNoError with too many parameters"
@@ -185,7 +185,7 @@ partial def getArity (e : Expr) : Nat :=
     `Meta.kabstract` invokes definitional equality, there were some instances in which `Meta.kabstract` performed
     an abstraction at a position where `RuleM.replace` would not perform a replacement. This was an issue because it
     created inconsistencies between the clauses produced by superposition's main code and proof reconstruction.
-    
+
     `abstractAtExpr` is written to follow the implementation of `Meta.kabstract` without invoking definitional equality
     (instead testing for equality after instantiating metavariables).  -/
 def Lean.Meta.abstractAtExpr (e : Expr) (p : Expr) (occs : Occurrences := .all) : MetaM Expr := do
@@ -219,4 +219,4 @@ def Lean.Meta.abstractAtExpr (e : Expr) (p : Expr) (occs : Occurrences := .all)
           visitChildren ()
       else
         visitChildren ()
-    visit e 0 |>.run' 1
+    visit e 0 |>.run' 1

lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9",
+   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "v4.15.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "35dd124945e6fe3bcd05ce6c5631c471fc23e164",
+   "rev": "997d810f10945740fb68923fbfa0cdf84636d07c",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "35dd124945e6fe3bcd05ce6c5631c471fc23e164",
+   "inputRev": "997d810f10945740fb68923fbfa0cdf84636d07c",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Duper",

lakefile.lean

@@ -2,8 +2,8 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"35dd124945e6fe3bcd05ce6c5631c471fc23e164"
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.14.0"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"997d810f10945740fb68923fbfa0cdf84636d07c"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.15.0"
 
 package Duper {
   precompileModules := true

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.14.0
+leanprover/lean4:v4.15.0