chore: adjust to lean4#3123

This removes an argument unused since leanprover/lean4#3123
leanprover-community · Jan 4, 2024 · 99334fa · 99334fa
1 parent 6940439
commit 99334fa
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 8 deletions.
diff --git a/Aesop/Index.lean b/Aesop/Index.lean
@@ -14,8 +14,8 @@ open Lean.Meta
 namespace Aesop
 
 structure Index (α : Type) [BEq α] [Hashable α] where
-  byTarget : DiscrTree α 
-  byHyp : DiscrTree α 
+  byTarget : DiscrTree α
+  byHyp : DiscrTree α
   unindexed : PHashSet α
   deriving Inhabited
 
@@ -56,9 +56,9 @@ partial def add (r : α) (imode : IndexingMode) (ri : Index α) :
   | IndexingMode.unindexed =>
     { ri with unindexed := ri.unindexed.insert r }
   | IndexingMode.target keys =>
-    { ri with byTarget := ri.byTarget.insertCore keys r discrTreeConfig }
+    { ri with byTarget := ri.byTarget.insertCore keys r }
   | IndexingMode.hyps keys =>
-    { ri with byHyp := ri.byHyp.insertCore keys r discrTreeConfig }
+    { ri with byHyp := ri.byHyp.insertCore keys r }
   | IndexingMode.or imodes =>
     imodes.foldl (init := ri) λ ri imode =>
       ri.add r imode

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "ee49cf8fada1bf5a15592c399a925c401848227f",
+   "rev": "0410d2762ab42a57fd8d7c98b73b87b7082dd65b",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "aesop",

diff --git a/lakefile.lean b/lakefile.lean
@@ -13,4 +13,4 @@ lean_lib AesopTest {
   globs := #[.submodules "AesopTest"]
 }
 
-require std from git "https://github.com/leanprover/std4" @ "main"
+require std from git "https://github.com/leanprover/std4" @ "nightly-testing"
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:nightly-2024-01-03
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.5.0-rc1
		leanprover/lean4:nightly-2024-01-03