opaque Lean.Meta.recExt : TagDeclarationExtension

Environment extension for storing which declarations are recursive. This information is populated by the PreDefinition module, but the simplifier uses when unfolding declarations.

def Lean.Meta.markAsRecursive (declName : Name) : CoreM Unit

Marks the given declaration as recursive.

def Lean.Meta.isRecursiveDefinition (declName : Name) : CoreM Bool

Returns true if declName was defined using well-founded recursion, or structural recursion.