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/Compilers/Named | |
parent | 9a3c43c13107b33ea7d109d23c83e81d414f84dd (diff) |
Allow specifying type in nlet
Diffstat (limited to 'src/Compilers/Named')
-rw-r--r-- | src/Compilers/Named/Syntax.v | 1 |
1 files changed, 1 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. |