# Documentation

• useDecide : Bool
• Check whether any of the hypotheses is an empty type.

emptyType : Bool
• When checking for empty types, searchFuel specifies the number of goals visited.

searchFuel : Nat
• Support for hypotheses such as

h : (x y : Nat) (ys : List Nat) → x = 0 → y::ys = [a, b, c] → False
→ x = 0 → y::ys = [a, b, c] → False
→ y::ys = [a, b, c] → False
→ False


This kind of hypotheses appear when proving conditional equation theorems for match expressions.

genDiseq : Bool
Instances For
@[inline]
Equations
Equations

Return true if goal mvarId has contradictory hypotheses. See MVarId.contradiction for the list of tests performed by this method.

Equations
• One or more equations did not get rendered due to their size.
def Lean.MVarId.contradiction (mvarId : Lean.MVarId) (config : optParam Lean.Meta.Contradiction.Config { useDecide := true, emptyType := true, searchFuel := 16, genDiseq := false }) :

Try to close the goal using "contradictions" such as

• Contradictory hypotheses h₁ : p and h₂ : ¬ p¬ p.
• Contradictory disequality h : x ≠ x≠ x.
• Contradictory equality between different constructors, e.g., h : List.nil = List.cons x xs.
• Empty inductive types, e.g., x : Fin 0.
• Decidable propositions that evaluate to false, i.e., a hypothesis h : p s.t. decide p reduces to false. This is only tried if Config.useDecide = true.

Throw exception if goal failed to be closed.

Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.contradiction (mvarId : Lean.MVarId) (config : optParam Lean.Meta.Contradiction.Config { useDecide := true, emptyType := true, searchFuel := 16, genDiseq := false }) :
Equations