From 2854cff14f95693819d42b611fe75a4904d9c77d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 13 May 2017 13:58:46 -0400 Subject: 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 --- src/Util/Notations.v | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'src/Util/Notations.v') 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"). -- cgit v1.2.3