structure Lean.Meta.Contradiction.Config : Type

• useDecide : Bool
• emptyType : Bool

  Check whether any of the hypotheses is an empty type.

• searchFuel : Nat

  When checking for empty types, searchFuel specifies the number of goals visited.

• genDiseq : Bool

  Support for hypotheses such as

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

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

@[reducible, inline]

abbrev Lean.Meta.ElimEmptyInductive.M (α : Type) : Type

instance Lean.Meta.ElimEmptyInductive.instMonadBacktrackSavedStateM : MonadBacktrack SavedState M

partial def Lean.Meta.ElimEmptyInductive.elim (mvarId : MVarId) (fvarId : FVarId) : M Bool

def Lean.Meta.mkGenDiseqMask (e : Expr) : Array Bool

Given e s.t. isGenDiseq e, generate a bit-mask mask s.t. mask[i] = true iff the i-th binder is an equality without forward dependencies.

See processGenDiseq

def Lean.Meta.mkGenDiseqMask.go (e : Expr) (acc : Array Bool) : Array Bool

def Lean.MVarId.contradictionCore (mvarId : MVarId) (config : Meta.Contradiction.Config) : MetaM Bool

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

def Lean.MVarId.contradiction (mvarId : MVarId) (config : Meta.Contradiction.Config := { }) : MetaM Unit

Try to close the goal using "contradictions" such as

• Contradictory hypotheses h₁ : p and h₂ : ¬ p.
• Contradictory disequality h : 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.