chore: update to Lean v4.12.0

tydeu · Oct 25, 2024 · 3c56f56 · 3c56f56
1 parent a712058
commit 3c56f56
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/Alloy/Util/OpaqueType.lean b/Alloy/Util/OpaqueType.lean
@@ -68,6 +68,7 @@ elab_rules : command
   let visibility ← liftMacroM <| expandOptVisibility vis?
   let safety := if uTk?.isSome then DefinitionSafety.unsafe else .safe
   let {declName, ..} ← expandDeclId declId {docString?, visibility}
+  let sc ← Command.getScope
   runTermElabM fun vars => do
   let stx ← getRef
   let nt ← if let some (some lv) := lv?? then
@@ -76,7 +77,7 @@ elab_rules : command
   let ntId := mkIdentFrom declId <| `_root_ ++ ntName
   let ntDefn := mkNode ``Parser.Command.declValSimple
     #[mkAtomFrom stx ":=", ← `(default_or_ofNonempty%)]
-  Term.elabMutualDef vars #[{
+  Term.elabMutualDef vars sc #[{
     ref := stx, headerRef := stx, kind := .opaque,
     modifiers := {isUnsafe := safety matches .unsafe},
     declId := declId.raw.setArg 0 ntId, binders := mkNullNode bs,

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.9.1
+leanprover/lean4:v4.12.0