Lean4
/-- The deriving handler for the `Countable` class.
Handles non-nested non-reflexive inductive types.
They can be mutual too — in that case, there is an optimization to re-use all the generated
functions and proofs.
-/
def mkCountableInstance (declNames : Array Name) : CommandElabM Bool := do
let mut seen : NameSet := { }
let mut toVisit : Array InductiveVal := #[]
for declName in declNames do
if seen.contains declName then
continue
let indVal ← getConstInfoInduct declName
if indVal.isNested || indVal.isReflexive then
return false
seen := seen.append (NameSet.ofList indVal.all)
toVisit := toVisit.push indVal
for indVal in toVisit do
let cmds ← liftTermElabM <| mkCountableCmds indVal (declNames.filter indVal.all.contains)
withEnableInfoTree false do
elabCommand <| mkNullNode cmds
return true
