Merge pull request #46 from lenianiva/misc/v4.12.0

feat: Update to Lean 4.12.0

Author: arthurpaulino

LSpec/SlimCheck/Checkable.lean

@@ -495,7 +495,7 @@ proposition where the quantifiers are annotated with `NamedBinder`.
 scoped elab "mk_decorations" : tactic => do
   let goalType ← (← getMainGoal).getType
   if let Expr.app (.const ``Decorations.DecorationsOf ..) body := goalType then
-    closeMainGoal (addDecorations body)
+    closeMainGoal `SlimCheck.mk_decorations (addDecorations body)
 
 end Decorations
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.4.0-rc1
+leanprover/lean4:v4.12.0