def Lean.Meta.Grind.isMatchCondCandidate (e : Expr) : Bool

Returns true if e is of the form ∀ ..., _ = _ ... -> False. The lhs of each equation must not have loose bound variables. Recall that the lhs should correspond to variables in a given alternative. For example, the given match-condition

∀ (head : Nat) (tail : List Nat), a = 1 → as = head :: tail → False

is generated for the second alternative at

def f : List Nat → List Nat → Nat
  | _, 1 :: _ :: _ => ...
  | _, a :: as => ...
  | _, _  => ...

That is, a must be different from 1, or as must not be of the form _ :: _. That is, they must not be a match for the first alternative. Note: We were not previously checking whether the lhs did not have loose bound variables. This missing check caused a panic at tryToProveFalse function at MatchCond.lean because it assumes the lhs does not have loose bound variables. Note: This function is an approximation. It may return true for terms that do not correspond to match-conditions.

Equations

• Lean.Meta.Grind.isMatchCondCandidate e = (e.isForall && Lean.Meta.Grind.isMatchCondCandidate.go✝ e)

def Lean.Meta.Grind.casesMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId)

Equations

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