- 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
Instances For
@[reducible, inline]
Equations
Instances For
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
Equations
Instances For
Return true
if goal mvarId
has contradictory hypotheses.
See MVarId.contradiction
for the list of tests performed by this method.
Equations
Instances For
Try to close the goal using "contradictions" such as
- Contradictory hypotheses
h₁ : p
andh₂ : ¬ 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 tofalse
. This is only tried ifConfig.useDecide = true
.
Throw exception if goal failed to be closed.