Update lean-auto

leanprover-community · Oct 14, 2024 · eed2d39 · eed2d39
1 parent 28406d9
commit eed2d39
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 3 deletions.
diff --git a/Duper/Tests/temp.lean b/Duper/Tests/temp.lean
@@ -13,6 +13,7 @@ open Lean Auto
 @[rebind Auto.Native.solverFunc]
 def Auto.duperPort (lemmas : Array Lemma) : MetaM Expr := do
   let formulas ← Duper.autoLemmasToFormulas lemmas
+  let formulas := formulas.map (fun f => (f.1, f.2.1, f.2.2.1, f.2.2.2, none))
   Duper.runDuperPortfolioMode formulas .none
     { portfolioMode := true,
       portfolioInstance := none,

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2b6ed7d9f86d558d94b8d9036a637395163c4fa6",
+   "rev": "6cd81c96800dc2d2741499e931f350f069ca74c7",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "2b6ed7d9f86d558d94b8d9036a637395163c4fa6",
+   "inputRev": "6cd81c96800dc2d2741499e931f350f069ca74c7",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",

diff --git a/lakefile.lean b/lakefile.lean
@@ -2,7 +2,7 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"2b6ed7d9f86d558d94b8d9036a637395163c4fa6"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"6cd81c96800dc2d2741499e931f350f069ca74c7"
 require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.11.0"
 
 package Duper {