def Lean.Elab.mkInstCCPOPProd (inst₁ inst₂ : Expr) : MetaM Expr

Equations

• Lean.Elab.mkInstCCPOPProd inst₁ inst₂ = Lean.Meta.mkAppOptM `Lean.Order.instCCPOPProd #[none, none, some inst₁, some inst₂]

def Lean.Elab.mkMonoPProd (hmono₁ hmono₂ : Expr) : MetaM Expr

Equations

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

def Lean.Elab.partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit

Equations

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