Documentation

Lean.Meta.Tactic.Contradiction

source
structure Lean.Meta.Contradiction.Config:
Type
  • 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 This kind of hypotheses appear when proving conditional equation theorems for match expressions.

    genDiseq : Bool
source
@[inline]
abbrev Lean.Meta.ElimEmptyInductive.M (α : Type) :
Type
Equations
source
instance Lean.Meta.ElimEmptyInductive.instMonadBacktrackSavedStateM:
Lean.MonadBacktrack Lean.Meta.SavedState Lean.Meta.ElimEmptyInductive.M
Equations
source
partial def Lean.Meta.ElimEmptyInductive.elim (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :
Lean.Meta.ElimEmptyInductive.M Bool
source
def Lean.Meta.contradictionCore (mvarId : Lean.MVarId) (config : Lean.Meta.Contradiction.Config) :
Lean.MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.contradiction (mvarId : Lean.MVarId) (config : optParam Lean.Meta.Contradiction.Config { useDecide := true, emptyType := true, searchFuel := 16, genDiseq := false }) :
Lean.MetaM Unit
Equations
  • One or more equations did not get rendered due to their size.