Mercurial > cpdt > repo

diff src/MoreSpecif.v @ 79:6c2607211cee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Expand MoreSpecif
author Adam Chlipala <adamc@hcoop.net>
date Fri, 03 Oct 2008 17:53:41 -0400
parents c49d999fe806
children fd505bcb5632
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