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

chore: add CollectLevelParams.visitLevels

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-24 08:19:30 -07:00
parent 81f8ab8fbb
commit 2cd21e08ba
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Util/CollectLevelParams.lean
View file

@ -31,6 +31,9 @@ mutual
| _ => id
end
def visitLevels (us : List Level) : Visitor :=
fun s => us.foldl (fun s u => visitLevel u s) s
mutual
partial def visitExpr (e : Expr) : Visitor := fun s =>
if !e.hasLevelParam then s
@ -44,7 +47,7 @@ mutual
| .letE _ t v b _ => visitExpr b ∘ visitExpr v ∘ visitExpr t
| .app f a => visitExpr a ∘ visitExpr f
| .mdata _ b => visitExpr b
| .const _ us => fun s => us.foldl (fun s u => visitLevel u s) s
| .const _ us => visitLevels us
| .sort u => visitLevel u
| _ => id
end