Documentation

Lean.Meta.Coe

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

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

Lean.Meta.expandCoe e = Lean.Meta.withReducibleAndInstances do let a ← Lean.Meta.transform e Lean.Meta.expandCoe.step fun e => pure (Lean.TransformStep.done e) pure a

partial def Lean.Meta.expandCoe.step (e : Lean.Expr) :

Lean.MetaM Lean.TransformStep