Skip to content

GitLab

S
stdpp
Merged
Opened by Robbert@robbertkrebbers
Report abuse

Pattern matching notation for monadic binds

This gets rid of the old hack to have specific notations for pairs up to a fixed arity, and moreover allows to do fancy things like:

Record test := Test { t1 : nat; t2 : nat }.

Definition foo (x : option test) : option nat :=
  ''(Test a1 a2) ← x;
  Some a1.

There are some problems, however:

  • It conflicts with Coq's notation ' x for Zpos x. Fortunately, the breakage is in the right direction: the proposed monadic notation breaks Coq's ' x. Furthermore, I believe said notation should be removed from Coq, see https://github.com/coq/coq/pull/6155
  • It breaks backwards compatibility. Since Coq only allows to use binders in recursive notations, the notation must start with at least one symbol, for which I picked '. As such, this means we need a double '.
Edited by Robbert