diff options
| -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" |