max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: size of a LocalContext

Browse source
This commit is contained in:
Scott Morrison 2022-07-19 14:24:21 +10:00 • committed by Leonardo de Moura
parent b9c0fd2ab3
commit aeeaaa6efc
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/LocalContext.lean
View file

@ -318,6 +318,9 @@ instance : ForIn m LocalContext LocalDecl where
@[inline] def foldr (lctx : LocalContext) (f : LocalDecl → β → β) (init : β) : β :=
Id.run <| lctx.foldrM f init
def size (lctx : LocalContext) : Nat :=
lctx.foldl (fun n _ => n+1) 0
@[inline] def findDecl? (lctx : LocalContext) (f : LocalDecl → Option β) : Option β :=
Id.run <| lctx.findDeclM? f