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/Compilers/Syntax.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/Compilers/Syntax.v')
| -rw-r--r-- | src/Compilers/Syntax.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/Syntax.v b/src/Compilers/Syntax.v index d8b88e560..0e8f924da 100644 --- a/src/Compilers/Syntax.v +++ b/src/Compilers/Syntax.v @@ -143,7 +143,7 @@ Module Export Notations. Notation "()" := (@Unit _) : ctype_scope. Notation "A * B" := (@Prod _ A B) : ctype_scope. Notation "A -> B" := (@Arrow _ A B) : ctype_scope. - Notation "'slet' x := A 'in' b" := (LetIn A (fun x => b)) : expr_scope. + Notation "'slet' x .. y := A 'in' b" := (LetIn A%expr (fun x => .. (fun y => b%expr) .. )) : expr_scope. Notation "'λ' x .. y , t" := (Abs (fun x => .. (Abs (fun y => t%expr)) ..)) : expr_scope. Notation "( x , y , .. , z )" := (Pair .. (Pair x%expr y%expr) .. z%expr) : expr_scope. Notation "( )" := TT : expr_scope. |