Skip to content

Commit

Permalink
Update lean-auto
Browse files Browse the repository at this point in the history
  • Loading branch information
JOSHCLUNE committed Oct 31, 2024
1 parent 25c3ea8 commit a500ea7
Show file tree
Hide file tree
Showing 4 changed files with 5 additions and 5 deletions.
2 changes: 1 addition & 1 deletion Duper/Tests/temp.lean
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ set_option auto.native true
open Lean Auto

@[rebind Auto.Native.solverFunc]
def Auto.duperPort (lemmas : Array Lemma) : MetaM Expr := do
def Auto.duperPort (lemmas inhLemmas : 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
Expand Down
2 changes: 1 addition & 1 deletion Duper/Tests/temp2.lean
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ set_option auto.native true
open Lean Auto

@[rebind Auto.Native.solverFunc]
def Auto.duperPort (lemmas : Array Lemma) : MetaM Expr := do
def Auto.duperPort (lemmas inhLemmas : 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
Expand Down
4 changes: 2 additions & 2 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,10 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "680d6d58ce2bb65d15e5711d93111b2e5b22cb1a",
"rev": "0728f384d78982e6fb0f1cdf263e172d3135e0be",
"name": "auto",
"manifestFile": "lake-manifest.json",
"inputRev": "680d6d58ce2bb65d15e5711d93111b2e5b22cb1a",
"inputRev": "0728f384d78982e6fb0f1cdf263e172d3135e0be",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/batteries",
Expand Down
2 changes: 1 addition & 1 deletion lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ import Lake

open Lake DSL

require auto from git "https://github.com/leanprover-community/lean-auto.git"@"680d6d58ce2bb65d15e5711d93111b2e5b22cb1a"
require auto from git "https://github.com/leanprover-community/lean-auto.git"@"0728f384d78982e6fb0f1cdf263e172d3135e0be"
require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.12.0"

package Duper {
Expand Down

0 comments on commit a500ea7

Please sign in to comment.