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

feat: add CodeDecl.dependsOn

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-03 19:36:26 -07:00
parent da4812659c
commit b3aff375f0
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/Compiler/LCNF/DependsOn.lean
View file

@ -31,6 +31,14 @@ private partial def depOn (c : Code) : M Bool :=
abbrev LetDecl.dependsOn (decl : LetDecl) (s : FVarIdSet) : Bool :=
decl.depOn s
abbrev FunDecl.dependsOn (decl : FunDecl) (s : FVarIdSet) : Bool :=
exprDepOn decl.type s || depOn decl.value s
def CodeDecl.dependsOn (decl : CodeDecl) (s : FVarIdSet) : Bool :=
match decl with
| .let decl => decl.dependsOn s
| .jp decl | .fun decl => decl.dependsOn s
/--
Return `true` is `c` depends on a free variable in `s`.
-/