Expand MoreSpecif

bc9ad81d · Adam Chlipala · 8823bade · bc9ad81d
Commit bc9ad81d authored Oct 03, 2008 by Adam Chlipala
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 0 deletions

MoreSpecif.v src/MoreSpecif.v +3 -0

No files found.
--- a/src/MoreSpecif.v
+++ b/src/MoreSpecif.v
@@ -40,6 +40,9 @@ Notation "x <- e1 ; e2" := (match e1 with
                           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