From b3aff375f0724228221194d355c535aa55c8d8ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Oct 2022 19:36:26 -0700 Subject: [PATCH] feat: add `CodeDecl.dependsOn` --- src/Lean/Compiler/LCNF/DependsOn.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Lean/Compiler/LCNF/DependsOn.lean b/src/Lean/Compiler/LCNF/DependsOn.lean index bbec31594f..baf134a959 100644 --- a/src/Lean/Compiler/LCNF/DependsOn.lean +++ b/src/Lean/Compiler/LCNF/DependsOn.lean @@ -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`. -/