chore: include recursor names in ConstantInfo.getUsedConstants

leanprover · Oct 3, 2023 · 9d9b313 · 9d9b313
1 parent a4aae91
commit 9d9b313
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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