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
_ => _ not
_ => anything else)
Should I report a bug? Because it's quite annoying I would say.
Last updated: Oct 04 2023 at 23:01 UTC