- Why ssreflect does’t use a
At the time Georges Gonthier introduced the
if t is pat then u else v syntax, the generic notation mechanism was not powerful enough to support it (because of the presence of a pattern in the notation, a feature which was introduced in 8.8.0 only).
- What is the motive for
IfNotations ? To be used in vanilla (non-ssreflect) coq?
I personally liked the idea of the notation
if t is pat then u else v a lot and wished that it was made available for all users, what was done in the
IfNotations module introduced in 8.8.0. There was a discussion on github about going further in unifying Georges’ non-reprinted version of
if t is pat then u else v in ssreflect and the printing-enabled version made available thanks to the support of patterns in the generic notation mechanism but it did not converge. If you think the merge effort should be continued to avoid the duplication, don’t hesitate to tell (see the discussion started here for more about what remains to be done to do a complete merge; it is mixed with other long and technical discussions though).
By the way, there are two reasons to have the “vanilla”
if is in a module. First because it introduces a new keyword
is and that may break compatibility in rare occasions (e.g. in
fun is : input_state => ...). Second, precisely because of an absence of convergence on the two implementations. Personally, I’d be happy in having
if is available by default for everyone (without requiring any