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.

Equations

• Lean.Meta.markAsRecursive declName = Lean.modifyEnv fun (x : Lean.Environment) => Lean.Meta.recExt.tag x declName

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

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

Equations

• Lean.Meta.isRecursiveDefinition declName = do let __do_lift ← Lean.getEnv pure (Lean.Meta.recExt.isTagged __do_lift declName)