Mercurial > cpdt > repo
changeset 79:6c2607211cee
Expand MoreSpecif
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 03 Oct 2008 17:53:41 -0400 |
parents | c49d999fe806 |
children | 506a06118014 |
files | src/MoreSpecif.v |
diffstat | 1 files changed, 3 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/src/MoreSpecif.v Fri Oct 03 15:59:59 2008 -0400 +++ b/src/MoreSpecif.v Fri Oct 03 17:53:41 2008 -0400 @@ -40,6 +40,9 @@ end) (right associativity, at level 60) : specif_scope. +Notation "!!" := (inright _ _) : specif_scope. +Notation "[[[ x ]]]" := (inleft _ [x]) : specif_scope. + Notation "x <-- e1 ; e2" := (match e1 with | inright _ => !! | inleft (exist x _) => e2