fix duper prelude in readme

leanprover-community · Nov 24, 2024 · 2511ca2 · 2511ca2
1 parent a50480e
commit 2511ca2
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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