Delab checking canonicity.

Provides a series of monadic functions in DelabM for delaborating expressions differently if their given instances differ (by definitional equality) with what is synthesized. Synthesized instances are considered 'canonical' for this purpose.

def Lean.Meta.isCanonicalInstance (inst : Expr) : MetaM Bool

Returns true iff the given instance is defeq to the instance synthesized for its type, and returns false otherwise (including if instance synthesis fails).

Equations

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

def delabCheckingCanonical : Lean.PrettyPrinter.Delaborator.DelabM (Bool × Lean.Term)

When the delab reader is pointed at an expression for an instance, returns (true, t) iff instance synthesis succeeds and produces a defeq instance; otherwise returns (false, t).

Equations

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

def Delab.Noncanonical.delabUnary (arity arg : Nat) (mkStx : Lean.Term → Lean.PrettyPrinter.Delaborator.Delab) : Lean.PrettyPrinter.Delaborator.Delab

Delaborate an expression with arity arity into a unary notation mkStx iff the argument arg is a non-canonical instance (is not defeq to what is synthesized for its type, or else instance synthesis fails).

Equations

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

def Delab.Noncanonical.delabBinary (arity arg₁ arg₂ : Nat) (mkStx : Lean.Term → Lean.Term → Lean.PrettyPrinter.Delaborator.DelabM Lean.Term) : Lean.PrettyPrinter.Delaborator.Delab

Delaborate an expression with arity arity into a binary notation mkStx iff either argument arg₁ or arg₂ are non-canonical instances (are not defeq to what is synthesized for its type, or else instance synthesis fails).

Equations

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