From 8f710abf9a8dc95be8bc7e3ad59749c3e14e7b62 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 16 Feb 2016 00:56:03 +0100 Subject: [PATCH] Missing heap_lang ;; notation for values. --- heap_lang/notation.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/heap_lang/notation.v b/heap_lang/notation.v index c235428c5..c332abc5e 100644 --- a/heap_lang/notation.v +++ b/heap_lang/notation.v @@ -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. Notation "e1 ;; e2" := (Lam "" e2%L e1%L) (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)) (at level 102, f, x, y at level 1, e at level 200) : lang_scope. -- GitLab