From e78a78ab287b89dfeb98eeee98aa6def242addeb Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Thu, 23 Jun 2016 13:55:39 +0200 Subject: [PATCH] heap_lang notations for Some/None. --- heap_lang/notation.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/heap_lang/notation.v b/heap_lang/notation.v index cf0c7db5c..0ebbc77e5 100644 --- a/heap_lang/notation.v +++ b/heap_lang/notation.v @@ -99,3 +99,17 @@ Notation "'let:' x := e1 'in' e2" := (LamV x%bind e2%E e1%E) (at level 102, x at level 1, e1, e2 at level 200) : val_scope. Notation "e1 ;; e2" := (LamV BAnon e2%E e1%E) (at level 100, e2 at level 200, format "e1 ;; e2") : val_scope. + +(** Notations for option *) +Notation NONE := (InjL #()). +Notation SOME x := (InjR x). + +Notation NONEV := (InjLV #()). +Notation SOMEV x := (InjRV x). + +Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" := + (Match e0 BAnon e1 x%bind e2) + (e0, e1, x, e2 at level 200) : expr_scope. +Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 | 'end'" := + (Match e0 BAnon e1 x%bind e2) + (e0, e1, x, e2 at level 200, only parsing) : expr_scope. -- GitLab