def Lean.Meta.isCoeDecl (declName : Lean.Name) : Bool

Return true iff declName is one of the auxiliary definitions/projections used to implement coercions.

Equations

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

def Lean.Meta.expandCoe (e : Lean.Expr) : Lean.MetaM Lean.Expr

Expand coercions occurring in e

Equations

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