bump to v4.15.0

Auto/Lib/MetaExtra.lean

@@ -23,6 +23,8 @@ partial def Meta.normalizeNondependentForall (e : Expr) : MetaM Expr := do
   let e' ← whnfNondependentForall e
   match e' with
   | .forallE name ty body bi =>
+    if body.hasLooseBVar 0 then
+      return e
     let ty' ← normalizeNondependentForall ty
     let body' ← normalizeNondependentForall body
     return .forallE name ty' body' bi
@@ -142,4 +144,16 @@ def Meta.exToExcept (x : MetaM α) : MetaM (Except Exception α) :=
 def Meta.runtimeExToExcept (x : MetaM α) : MetaM (Except Exception α) :=
   tryCatchRuntimeEx (do let v ← x; return .ok v) (fun e => return .error e)
 
+/--
+  Workaround for modifying the `lctx` field of `Meta.Context`
+-/
+def Meta.Context.modifyLCtx (ctx : Context) (lctx : LocalContext) : CoreM Context :=
+  MetaM.run' (withLCtx' lctx read) ctx
+
+/--
+  Workaround for modifying the `localInstances` field of `Meta.Context`
+-/
+def Meta.Context.modifyLocalInstances (ctx : Context) (localInsts : LocalInstances) : CoreM Context :=
+  MetaM.run' (withLCtx ctx.lctx localInsts read) ctx
+
 end Auto

Auto/Lib/MetaState.lean

@@ -76,7 +76,7 @@ private def runWithFVars (lctx : LocalContext) (fvarids : Array FVarId) (k : Met
       | .ldecl _ fvarId userName type value nonDep kind =>
         newlctx := newlctx.mkLetDecl fvarId userName type value nonDep kind
     | .none => throwError "{decl_name%} :: Unknown free variable {Expr.fvar fid}"
-  withReader (fun ctx => {ctx with lctx := newlctx}) k
+  Meta.withLCtx' newlctx k
 
 private def runWithIntroducedFVarsImp (m : MetaStateM (Array FVarId × α)) (k : α → MetaM β) : MetaM β := do
   let s ← get
@@ -116,19 +116,22 @@ def mkLocalDecl (fvarId : FVarId) (userName : Name) (type : Expr)
   (bi : BinderInfo := BinderInfo.default) (kind : LocalDeclKind := LocalDeclKind.default) : MetaStateM Unit := do
   let ctx ← getToContext
   let lctx := ctx.lctx
-  setToContext ({ctx with lctx := lctx.mkLocalDecl fvarId userName type bi kind})
+  let newCtx ← Meta.Context.modifyLCtx ctx (lctx.mkLocalDecl fvarId userName type bi kind)
+  setToContext newCtx
 
 def mkLetDecl (fvarId : FVarId) (userName : Name) (type value : Expr)
   (nonDep : Bool := false) (kind : LocalDeclKind := default) : MetaStateM Unit := do
   let ctx ← getToContext
   let lctx := ctx.lctx
-  setToContext ({ctx with lctx := lctx.mkLetDecl fvarId userName type value nonDep kind})
+  let newCtx ← Meta.Context.modifyLCtx ctx (lctx.mkLetDecl fvarId userName type value nonDep kind)
+  setToContext newCtx
 
 private def withNewLocalInstance (className : Name) (fvar : Expr) : MetaStateM Unit := do
   let localDecl ← runMetaM <| Meta.getFVarLocalDecl fvar
   if !localDecl.isImplementationDetail then
     let ctx ← getToContext
-    setToContext ({ ctx with localInstances := ctx.localInstances.push { className := className, fvar := fvar } })
+    let newCtx ← Meta.Context.modifyLocalInstances ctx (ctx.localInstances.push { className := className, fvar := fvar })
+    setToContext newCtx
 
 private def withNewFVar (fvar fvarType : Expr) : MetaStateM Unit := do
   if let some c ← runMetaM <| Meta.isClass? fvarType then
@@ -149,10 +152,12 @@ def withLetDecl (n : Name) (type : Expr) (val : Expr) (kind : LocalDeclKind) : M
   return fvarId
 
 def withTemporaryLCtx [MonadLiftT MetaStateM n] [Monad n] (lctx : LocalContext) (localInsts : LocalInstances) (k : n α) : n α := do
-  let initlctx ← getToContext
-  MetaState.setToContext {initlctx with lctx := lctx, localInstances := localInsts}
+  let initCtx ← getToContext
+  let newCtx ← (Meta.Context.modifyLCtx initCtx lctx : MetaStateM _)
+  let newCtx ← (Meta.Context.modifyLocalInstances newCtx localInsts : MetaStateM _)
+  MetaState.setToContext newCtx
   let ret ← k
-  MetaState.setToContext initlctx
+  MetaState.setToContext initCtx
   return ret
 
 end Auto.MetaState

lean-toolchain

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