From a500ea7a5b9eca0ecaa7b4a229786a61b2707d30 Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Thu, 31 Oct 2024 00:44:36 -0400
Subject: [PATCH] Update lean-auto

---
 Duper/Tests/temp.lean  | 2 +-
 Duper/Tests/temp2.lean | 2 +-
 lake-manifest.json     | 4 ++--
 lakefile.lean          | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Duper/Tests/temp.lean b/Duper/Tests/temp.lean
index 6d97f20..d08366c 100644
--- a/Duper/Tests/temp.lean
+++ b/Duper/Tests/temp.lean
@@ -11,7 +11,7 @@ set_option auto.native true
 open Lean Auto
 
 @[rebind Auto.Native.solverFunc]
-def Auto.duperPort (lemmas : Array Lemma) : MetaM Expr := do
+def Auto.duperPort (lemmas inhLemmas : Array Lemma) : MetaM Expr := do
   let formulas ← Duper.autoLemmasToFormulas lemmas
   let formulas := formulas.map (fun f => (f.1, f.2.1, f.2.2.1, f.2.2.2, none))
   Duper.runDuperPortfolioMode formulas .none
diff --git a/Duper/Tests/temp2.lean b/Duper/Tests/temp2.lean
index 88c52f7..f00a418 100644
--- a/Duper/Tests/temp2.lean
+++ b/Duper/Tests/temp2.lean
@@ -11,7 +11,7 @@ set_option auto.native true
 open Lean Auto
 
 @[rebind Auto.Native.solverFunc]
-def Auto.duperPort (lemmas : Array Lemma) : MetaM Expr := do
+def Auto.duperPort (lemmas inhLemmas : Array Lemma) : MetaM Expr := do
   let formulas ← Duper.autoLemmasToFormulas lemmas
   let formulas := formulas.map (fun f => (f.1, f.2.1, f.2.2.1, f.2.2.2, none))
   Duper.runDuperPortfolioMode formulas .none
diff --git a/lake-manifest.json b/lake-manifest.json
index 3a19deb..585682b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "680d6d58ce2bb65d15e5711d93111b2e5b22cb1a",
+   "rev": "0728f384d78982e6fb0f1cdf263e172d3135e0be",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "680d6d58ce2bb65d15e5711d93111b2e5b22cb1a",
+   "inputRev": "0728f384d78982e6fb0f1cdf263e172d3135e0be",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
diff --git a/lakefile.lean b/lakefile.lean
index 9416246..3cd8544 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,7 +2,7 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"680d6d58ce2bb65d15e5711d93111b2e5b22cb1a"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"0728f384d78982e6fb0f1cdf263e172d3135e0be"
 require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.12.0"
 
 package Duper {