fix name clash with Std.Lean.CoreM

leanprover-community · Nov 4, 2023 · a0a6e84 · a0a6e84
1 parent bb3129b
commit a0a6e84
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 2 deletions.
diff --git a/Duper/Interface.lean b/Duper/Interface.lean
@@ -1,3 +1,4 @@
+import Std.Lean.CoreM
 import Duper.ProofReconstruction
 
 open Lean
@@ -196,8 +197,6 @@ def runDuperInstance4 (formulas : List (Expr × Expr × Array Name)) (inhabitati
   | none => withOptions (fun o => o.set `selFunction 13) $ runDuper formulas instanceMaxHeartbeats
   | some b => withOptions (fun o => (o.set `selFunction 13).set `inhabitationReasoning b) $ runDuper formulas instanceMaxHeartbeats
 
-def getMaxHeartbeats : CoreM Nat := return (← read).maxHeartbeats
-
 declare_syntax_cat Duper.bool_lit (behavior := symbol)
 
 syntax "true" : Duper.bool_lit

diff --git a/DuperOnMathlib/lake-manifest.json b/DuperOnMathlib/lake-manifest.json
@@ -49,5 +49,13 @@
     "opts": {},
     "name": "proofwidgets",
     "inputRev?": "v0.0.19",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/lean-auto.git",
+    "subDir?": null,
+    "rev": "db8a6b790b25724c36e6f698830f6d2238f2b6a0",
+    "opts": {},
+    "name": "auto",
+    "inputRev?": "main",
     "inherited": true}}],
  "name": "duperOnMathlib"}