chore: bump Lean v4.9.1

tydeu · Jul 16, 2024 · 7af65d3 · 7af65d3
1 parent d93e059
commit 7af65d3
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/Alloy/Util/OpaqueType.lean b/Alloy/Util/OpaqueType.lean
@@ -62,21 +62,22 @@ syntax (name := opaqueType)
 "opaque_type " declId binders (typeLvSpec)? : command
 
 elab_rules : command
-| `(opaqueType| $(doc?)? $(attrs?)? $(vis?)? $[unsafe%$uTk?]? opaque_type $declId $bs* $[: Type $(lv??)?]?)  => do
+| `(opaqueType| $(doc?)? $(attrs?)? $(vis?)? $[unsafe%$uTk?]? opaque_type $declId $bs* $[: Type $(lv??)?]?) => do
   let docString? ← doc?.mapM getDocStringText
   let attrs ← if let some attrs := attrs? then elabDeclAttrs attrs else pure #[]
   let visibility ← liftMacroM <| expandOptVisibility vis?
   let safety := if uTk?.isSome then DefinitionSafety.unsafe else .safe
   let {declName, ..} ← expandDeclId declId {docString?, visibility}
   runTermElabM fun vars => do
+  let stx ← getRef
   let nt ← if let some (some lv) := lv?? then
     `(NonemptyType.{$lv}) else `(NonemptyType.{0})
   let ntName := declName.str "nonemptyType"
   let ntId := mkIdentFrom declId <| `_root_ ++ ntName
   let ntDefn := mkNode ``Parser.Command.declValSimple
-    #[mkAtomFrom (← getRef) ":=", ← `(default_or_ofNonempty%)]
+    #[mkAtomFrom stx ":=", ← `(default_or_ofNonempty%)]
   Term.elabMutualDef vars #[{
-    ref := (← getRef), kind := .opaque,
+    ref := stx, headerRef := stx, kind := .opaque,
     modifiers := {isUnsafe := safety matches .unsafe},
     declId := declId.raw.setArg 0 ntId, binders := mkNullNode bs,
     type? := nt, value := ntDefn

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