Skip to content
Snippets Groups Projects
Commit 8f710abf authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Missing heap_lang ;; notation for values.

parent f6ad3a33
No related branches found
No related tags found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 0 deletions
heap_lang/notation.v
+ 2
− 0
View file @ 8f710abf
...@@ -56,6 +56,8 @@ Notation "'let:' x := e1 'in' e2" := (LamV x e2%L e1%L) ...@@ -56,6 +56,8 @@ Notation "'let:' x := e1 'in' e2" := (LamV x e2%L e1%L)
(at level 102, x at level 1, e1, e2 at level 200) : lang_scope. (at level 102, x at level 1, e1, e2 at level 200) : lang_scope.
Notation "e1 ;; e2" := (Lam "" e2%L e1%L) Notation "e1 ;; e2" := (Lam "" e2%L e1%L)
(at level 100, e2 at level 200) : lang_scope. (at level 100, e2 at level 200) : lang_scope.
Notation "e1 ;; e2" := (LamV "" e2%L e1%L)
(at level 100, e2 at level 200) : lang_scope.
Notation "'rec:' f x y := e" := (Rec f x (Lam y e%L)) Notation "'rec:' f x y := e" := (Rec f x (Lam y e%L))
(at level 102, f, x, y at level 1, e at level 200) : lang_scope. (at level 102, f, x, y at level 1, e at level 200) : lang_scope.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment