def Lean.Meta.Grind.isDiseq (a b : Expr) : GoalM Bool

Returns true if a and b are known to be disequal. See getDiseqFor?

Equations

• Lean.Meta.Grind.isDiseq a b = do let __do_lift ← Lean.Meta.Grind.getDiseqFor?✝ a b pure __do_lift.isSome

def Lean.Meta.Grind.mkDiseqProof? (a b : Expr) : GoalM (Option Expr)

Returns a proof for true if a and b are known to be disequal. See getDiseqFor?

Equations

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