change Duper.run invocation in README.md

Author: PratherConid

Auto/EvaluateAuto/TestAuto.lean

@@ -233,7 +233,7 @@ def leanFileLinesCallingRunAutoOnConsts
     "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))",
-    "  Duper.runDuper lemmas.toList 0",
+    "  Duper.runDuper lemmas.toList [] 0",
     "",
     "attribute [rebind Auto.Native.solverFunc] Auto.duperRaw",
     "",

README.md

@@ -13,7 +13,7 @@ open Lean Auto in
 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))
-  Duper.runDuper lemmas.toList 0
+  Duper.runDuper lemmas.toList [] 0
 
 attribute [rebind Auto.Native.solverFunc] Auto.duperRaw
 set_option auto.native true