Documentation

Lean.Meta.Coe

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

Equations

Lean.Meta.isCoeDecl declName = (declName == `Coe.coe || declName == `CoeTC.coe || declName == `CoeHead.coe || declName == `CoeTail.coe || declName == `CoeHTCT.coe || declName == `CoeDep.coe || declName == `CoeT.coe || declName == `CoeFun.coe || declName == `CoeSort.coe || declName == `Lean.Internal.liftCoeM || declName == `Lean.Internal.coeM)

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

Lean.MetaM Lean.Expr

Equations

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

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

Lean.MetaM Lean.TransformStep