From 2511ca29f39488a89eae6d7cdc0b995dd170304d Mon Sep 17 00:00:00 2001
From: PratherConid <syxx2013050321@163.com>
Date: Sun, 24 Nov 2024 00:36:29 -0800
Subject: [PATCH] fix duper prelude in readme

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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