diff --git a/README.md b/README.md index 342598c..210f5d8 100644 --- a/README.md +++ b/README.md @@ -10,10 +10,10 @@ import Auto.Tactic import Duper.Tactic open Lean Auto in -def Auto.duperRaw (lemmas : Array Lemma) (_ : Array Lemma) : MetaM Expr := do +def Auto.duperRaw (lemmas : Array Lemma) (inhs : Array Lemma) : MetaM Expr := do let lemmas : Array (Expr × Expr × Array Name × Bool) ← lemmas.mapM (fun ⟨⟨proof, ty, _⟩, _⟩ => do return (ty, ← Meta.mkAppM ``eq_true #[proof], #[], true)) - runDuper lemmas.data 0 + Duper.runDuper lemmas.toList 0 attribute [rebind Auto.Native.solverFunc] Auto.duperRaw set_option auto.native true