diff options
author | Jason Gross <jgross@mit.edu> | 2017-05-14 11:09:38 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-05-14 11:09:38 -0400 |
commit | f0aa1a484ecdc01c4aedd1a1ad75324619bc0456 (patch) | |
tree | b0b3cd29ec8549e7989e2439ec99e981f58ceeec /src | |
parent | 9a3c43c13107b33ea7d109d23c83e81d414f84dd (diff) |
Allow specifying type in nlet
Diffstat (limited to 'src')
-rw-r--r-- | src/Compilers/Named/Syntax.v | 1 | ||||
-rw-r--r-- | src/Util/Notations.v | 2 |
2 files changed, 3 insertions, 0 deletions
diff --git a/src/Compilers/Named/Syntax.v b/src/Compilers/Named/Syntax.v index a79628cb2..993a5cc77 100644 --- a/src/Compilers/Named/Syntax.v +++ b/src/Compilers/Named/Syntax.v @@ -86,6 +86,7 @@ Global Arguments interp {_ _ _ _ _ interp_op ctx t} _ _. Global Arguments Interp {_ _ _ _ _ interp_op t} _ _. Notation "'nlet' x := A 'in' b" := (LetIn _ x A%nexpr b%nexpr) : nexpr_scope. +Notation "'nlet' x : tx := A 'in' b" := (LetIn tx x A%nexpr b%nexpr) : nexpr_scope. Notation "'λn' x .. y , t" := (Abs x .. (Abs y t%nexpr) .. ) : nexpr_scope. Notation "( x , y , .. , z )" := (Pair .. (Pair x%nexpr y%nexpr) .. z%nexpr) : nexpr_scope. Notation "()" := TT : nexpr_scope. diff --git a/src/Util/Notations.v b/src/Util/Notations.v index feffc0f4b..f6dc432b8 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -71,6 +71,8 @@ Reserved Notation "'plet' x := y 'in' z" (at level 200, z at level 200, format "'plet' x := y 'in' '//' z"). Reserved Notation "'nlet' x := A 'in' b" (at level 200, b at level 200, format "'nlet' x := A 'in' '//' b"). +Reserved Notation "'nlet' x : tx := A 'in' b" + (at level 200, b at level 200, format "'nlet' x : tx := 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" |