Consider the following:
Require Import ssreflect.
Goal forall b : bool, (if b then 0 else 1) = 1.
Proof.
Fail lazymatch goal with
| |- context [ if _ then _ else ?xx ] =>
idtac
end.
lazymatch goal with
| |- context [ if _ then ?xx else _ ] =>
idtac
end.
Matching on the content of the left branch is fine, but not in the right one. It fails with "Non supported pattern". (At least for 8.14.)
it seems the ssreflect boolean_if_scope if
produces something like match _ with true => _ | _ => ?xx end
after notation interpretation, and pattern_of_glob_scope can only handle default cases if they produce _
(ie _ => _
not _ => anything else
)
Should I report a bug? Because it's quite annoying I would say.
Last updated: Oct 13 2024 at 01:02 UTC