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

Returns some (c = d) if

• c = d and False are in the same equivalence class, and
• a (b) and c are in the same equivalence class, and
• b (a) and d are in the same equivalence class. Otherwise return none.

Remark a and b are assumed to have the same type.

Equations

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

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.mkDiseqProofUsing (a b eq : Expr) : GoalM Expr

Given an equality eq of the form c = d s.t. eq is False, and a = b is congruent to c = d, return a proof for a ≠ b

Equations

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

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.

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

Equations

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