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 | |
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')
-rw-r--r-- | src/Util/LetIn.v | 6 | ||||
-rw-r--r-- | src/Util/Notations.v | 14 |
2 files changed, 11 insertions, 9 deletions
diff --git a/src/Util/LetIn.v b/src/Util/LetIn.v index 69cacd75e..92c7b51ad 100644 --- a/src/Util/LetIn.v +++ b/src/Util/LetIn.v @@ -5,12 +5,12 @@ Require Import Crypto.Util.Notations. Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. Definition Let_In_pf {A P} (x : A) (f : forall a : A, a = x -> P a) : P x := let y := x in f y eq_refl. -Notation "'dlet_nd' x := y 'in' f" := (Let_In (P:=fun _ => _) y (fun x => f)) (only parsing). -Notation "'dlet' x := y 'in' f" := (Let_In y (fun x => f)). +Notation "'dlet_nd' x .. y := v 'in' f" := (Let_In (P:=fun _ => _) v (fun x => .. (fun y => f) .. )) (only parsing). +Notation "'dlet' x .. y := v 'in' f" := (Let_In v (fun x => .. (fun y => f) .. )). Notation "'pflet' x , pf := y 'in' f" := (Let_In_pf y (fun x pf => f)). Module Bug5107WorkAround. - Notation "'dlet' x := y 'in' f" := (Let_In (P:=fun _ => _) y (fun x => f)). + Notation "'dlet' x .. y := v 'in' f" := (Let_In (P:=fun _ => _) v (fun x => .. (fun y => f) .. )). End Bug5107WorkAround. Global Instance Proper_Let_In_nd_changebody {A P R} {Reflexive_R:@Reflexive P R} 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"). |