Helper function for synthesizing order related instances.

def Lean.Meta.Grind.mkLawfulOrderLTInst? (u : Level) (type : Expr) (ltInst? leInst? : Option Expr) : GoalM (Option Expr)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.mkLawfulOrderLTInst? u type (some inst) leInst? = pure none
• Lean.Meta.Grind.mkLawfulOrderLTInst? u type ltInst? leInst? = pure none

def Lean.Meta.Grind.mkIsPreorderInst? (u : Level) (type : Expr) (leInst? : Option Expr) : GoalM (Option Expr)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.mkIsPreorderInst? u type leInst? = pure none

def Lean.Meta.Grind.mkIsPartialOrderInst? (u : Level) (type : Expr) (leInst? : Option Expr) : GoalM (Option Expr)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.mkIsPartialOrderInst? u type leInst? = pure none

def Lean.Meta.Grind.mkIsLinearOrderInst? (u : Level) (type : Expr) (leInst? : Option Expr) : GoalM (Option Expr)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.mkIsLinearOrderInst? u type leInst? = pure none

def Lean.Meta.Grind.mkIsLinearPreorderInst? (u : Level) (type : Expr) (leInst? : Option Expr) : GoalM (Option Expr)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.mkIsLinearPreorderInst? u type leInst? = pure none