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

feat: add LocalContext.foldrM

Browse source
This commit is contained in:
Leonardo de Moura 2021-12-02 17:19:30 -08:00
parent bb768b06cd
commit bf3a1e94a9
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/LocalContext.lean
View file

@ -262,6 +262,11 @@ def getAt? (lctx : LocalContext) (i : Nat) : Option LocalDecl :=
| none => pure b
| some decl => f b decl
@[specialize] def foldrM [Monad m] (lctx : LocalContext) (f : LocalDecl → β → m β) (init : β) : m β :=
lctx.decls.foldrM (init := init) fun decl b => match decl with
| none => pure b
| some decl => f decl b
@[specialize] def forM [Monad m] (lctx : LocalContext) (f : LocalDecl → m PUnit) : m PUnit :=
lctx.decls.forM fun decl => match decl with
| none => pure PUnit.unit
@ -285,6 +290,9 @@ instance : ForIn m LocalContext LocalDecl where
@[inline] def foldl (lctx : LocalContext) (f : β → LocalDecl → β) (init : β) (start : Nat := 0) : β :=
Id.run <| lctx.foldlM f init start
@[inline] def foldr (lctx : LocalContext) (f : LocalDecl → β → β) (init : β) : β :=
Id.run <| lctx.foldrM f init
@[inline] def findDecl? (lctx : LocalContext) (f : LocalDecl → Option β) : Option β :=
Id.run <| lctx.findDeclM? f