chore: bump batteries, follow deprecations (#179)

leanprover-community · Nov 14, 2024 · de91b59 · de91b59
1 parent 39119d2
commit de91b59
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean
@@ -89,7 +89,7 @@ def getConclusionDiscrTreeKeys (type : Expr) (config : WhnfCoreConfig) :
 -- For a constant `d` with type `∀ (x₁, ..., xₙ), T`, returns keys that
 -- match `d * ... *` (with `n` stars).
 def getConstDiscrTreeKeys (decl : Name) : MetaM (Array Key) := do
-  let arity := (← getConstInfo decl).type.forallArity
+  let arity := (← getConstInfo decl).type.getNumHeadForalls
   let mut keys := Array.mkEmpty (arity + 1)
   keys := keys.push $ .const decl arity
   for _ in [0:arity] do

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "76e9ebe4176d29cb9cc89c669ab9f1ce32b33c3d",
+   "rev": "b100ff2565805e9f30a482788b3fc66937a7f38a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",