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

fix: remove fix2

Browse source
This commit is contained in:
E.W.Ayers 2022-06-16 18:26:41 -04:00 • committed by Leonardo de Moura
parent 18ba16ded9
commit ee6ba180ea
1 changed files with 10 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/Lean/SubExpr.lean
View file

@ -47,20 +47,21 @@ def push (p : Pos) (c : Nat) : Pos :=
variable {α : Type} [Inhabited α]
/-- Fold over the position starting at the root and heading to the leaf-/
def foldl (f : α → Nat → α) : α → Pos → α :=
fix2 (fun r a p => if p.isRoot then a else f (r a p.tail) p.head)
partial def foldl (f : α → Nat → α) (a : α) (p : Pos) : α :=
if p.isRoot then a else f (foldl f a p.tail) p.head
/-- Fold over the position starting at the leaf and heading to the root-/
def foldr (f : Nat → α → α) : Pos → α → α :=
fix2 (fun r p a => if p.isRoot then a else r p.tail (f p.head a))
partial def foldr (f : Nat → α → α) (p : Pos) (a : α) : α :=
if p.isRoot then a else foldr f p.tail (f p.head a)
/-- monad-fold over the position starting at the root and heading to the leaf-/
def foldlM [Monad M] (f : α → Nat → M α) : α → Pos → M α :=
fix2 (fun r a p => if p.isRoot then pure a else do f (← r a p.tail) p.head)
/-- monad-fold over the position starting at the root and heading to the leaf -/
partial def foldlM [Monad M] (f : α → Nat → M α) (a : α) (p : Pos) : M α :=
have : Inhabited (M α) := inferInstance
if p.isRoot then pure a else do foldlM f a p.tail >>= (f · p.head)
/-- monad-fold over the position starting at the leaf and finishing at the root. -/
def foldrM [Monad M] (f : Nat → α → M α) : Pos → α → M α :=
fix2 (fun r p a => if p.isRoot then pure a else f p.head a >>= r p.tail)
partial def foldrM [Monad M] (f : Nat → α → M α) (p : Pos) (a : α) : M α :=
if p.isRoot then pure a else f p.head a >>= foldrM f p.tail
def depth (p : Pos) :=
p.foldr (fun _ => Nat.succ) 0