Skip to content

Commit

Permalink
Updating version on README
Browse files Browse the repository at this point in the history
  • Loading branch information
JOSHCLUNE committed Apr 18, 2024
1 parent 169bbb5 commit 98cc99f
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion Duper/Interface.lean
Original file line number Diff line number Diff line change
Expand Up @@ -418,7 +418,7 @@ partial def getLeavesFromDTr (t : Auto.DTr) : Array String :=
track of `isFromGoal` information through the monomorphization procedure. -/
def formulasToAutoLemmas (formulas : List (Expr × Expr × Array Name × Bool)) : MetaM (Array Auto.Lemma) :=
formulas.toArray.mapM
(fun (fact, proof, params, isFromGoal) => -- For now, isFromGoal is ignored
(fun (fact, proof, params, isFromGoal) =>
return {proof := ← Meta.mkAppM ``of_eq_true #[proof], type := fact, params := params, deriv := (.leaf s!"{isFromGoal}")})

/-- Converts formulas/lemmas from the format used by Auto to the format used by Duper. -/
Expand Down
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ Duper is an automatic proof-producing theorem prover broadly similar to Isabelle
To use Duper in an existing Lean 4 project, first add this package as a dependency. In your lakefile.lean, add:

```lean
require Duper from git "https://github.com/leanprover-community/duper.git" @ "v0.0.10"
require Duper from git "https://github.com/leanprover-community/duper.git" @ "v0.0.11"
```

Then, make sure that your `lean-toolchain` file contains the same version of Lean 4 as Duper and that if your project imports [std4](https://github.com/leanprover/std4.git), then it uses the same version of std4 as the Duper branch of [Auto](https://github.com/leanprover-community/lean-auto.git). This step is necessary because Duper depends on Auto which depends on std4, so errors can arise if your project attempts to import a version of std4 different from the one imported by Duper.
Expand Down

0 comments on commit 98cc99f

Please sign in to comment.