diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-13 13:58:46 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-13 13:58:46 -0400 |
| commit | 2854cff14f95693819d42b611fe75a4904d9c77d (patch) | |
| tree | c105298f538c87a2bd0ac19d1a4e273827e0709d /src/Util/Notations.v | |
| parent | de7a98b8711f13f9b9bba016c1d19db730479c8e (diff) | |
Support destructuring dlet and slet
The current way to support it is a kludge around the fact that `x
binder` only works for recursive notations
Diffstat (limited to 'src/Util/Notations.v')
| -rw-r--r-- | src/Util/Notations.v | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/Util/Notations.v b/src/Util/Notations.v index ca593edac..feffc0f4b 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -69,17 +69,19 @@ Reserved Notation "u {{ i }}" (at level 30). Reserved Notation "a # b" (at level 55, no associativity). (* match with theories/QArith/QArith_base.v *) Reserved Notation "'plet' x := y 'in' z" (at level 200, z at level 200, format "'plet' x := y 'in' '//' z"). -Reserved Notation "'slet' x := A 'in' b" - (at level 200, b at level 200, format "'slet' x := A 'in' '//' b"). +Reserved Notation "'nlet' x := A 'in' b" + (at level 200, b at level 200, format "'nlet' x := A 'in' '//' b"). +Reserved Notation "'slet' x .. y := A 'in' b" + (at level 200, x binder, y binder, b at level 200, format "'slet' x .. y := A 'in' '//' b"). Reserved Notation "'llet' x := A 'in' b" (at level 200, b at level 200, format "'llet' x := A 'in' '//' b"). Reserved Notation "'mlet' x := A 'in' b" (at level 200, b at level 200, format "'mlet' x := A 'in' '//' b"). (* Note that making [Let] a keyword breaks the vernacular [Let] in Coq 8.4 *) -Reserved Notation "'dlet_nd' x := y 'in' f" - (at level 200, f at level 200, format "'dlet_nd' x := y 'in' '//' f"). -Reserved Notation "'dlet' x := y 'in' f" - (at level 200, f at level 200, format "'dlet' x := y 'in' '//' f"). +Reserved Notation "'dlet_nd' x .. y := v 'in' f" + (at level 200, x binder, y binder, f at level 200, format "'dlet_nd' x .. y := v 'in' '//' f"). +Reserved Notation "'dlet' x .. y := v 'in' f" + (at level 200, x binder, y binder, f at level 200, format "'dlet' x .. y := v 'in' '//' f"). Reserved Notation "'pflet' x , pf := y 'in' f" (at level 200, f at level 200, format "'pflet' x , pf := y 'in' '//' f"). Reserved Notation "'λ' x .. y , t" (at level 200, x binder, y binder, right associativity, format "'λ' x .. y , '//' t"). |