Reification Bridge Normalization

The reflected expression is often definitionally related to the user's term but not syntactically identical: custom wrappers were unfolded, subtraction was lowered to addition and negation, and powers became multiplication. This module centralizes that final, proof-producing conversion.

def LeanCert.Tactic.unfoldReifiedDefinitions (unfolded : Array Lean.Name) : Lean.Elab.Tactic.TacticM Unit

Delta-reduce exactly the user definitions recorded by reification.

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Tactic.closeReificationBridge (report : Meta.ReifyReport) : Lean.Elab.Tactic.TacticM Unit

Close a semantic bridge between a user's real expression and its reflected LeanCert.Core.Expr.eval form.

Only definitions actually unfolded by the reifier are delta-reduced. The remaining normalization is a fixed, auditable collection of evaluation and ordinary arithmetic identities.

Equations

• One or more equations did not get rendered due to their size.