diff --git a/Lean4Checker/Lean.lean b/Lean4Checker/Lean.lean index 3a593da..30f0fe1 100644 --- a/Lean4Checker/Lean.lean +++ b/Lean4Checker/Lean.lean @@ -44,6 +44,7 @@ def getUsedConstants (c : ConstantInfo) : NameSet := | .inductInfo val => .ofList val.ctors | .opaqueInfo val => val.value.getUsedConstants' | .ctorInfo val => ({} : NameSet).insert val.name + | .recInfo val => .ofList val.all | _ => {} def inductiveVal! : ConstantInfo → InductiveVal