Mercurial > cpdt > repo
diff src/MoreSpecif.v @ 335:1f57a8d0ed3d
Pass over Subset
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 05 Oct 2011 11:32:13 -0400 |
| parents | 54e8ecb5ec88 |
| children | ad315efc3b6b |
line wrap: on
line diff
--- a/src/MoreSpecif.v Tue Oct 04 13:38:21 2011 -0400 +++ b/src/MoreSpecif.v Wed Oct 05 11:32:13 2011 -0400 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008, 2011, Adam Chlipala * * This work is licensed under a * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 @@ -51,7 +51,7 @@ Notation "{{ x | P }}" := (maybe (fun x => P)) : specif_scope. Notation "??" := (Unknown _) : specif_scope. -Notation "[[ x ]]" := (Found _ x _) : specif_scope. +Notation "[| x |]" := (Found _ x _) : specif_scope. Notation "x <- e1 ; e2" := (match e1 with | Unknown => ?? @@ -60,7 +60,7 @@ (right associativity, at level 60) : specif_scope. Notation "!!" := (inright _ _) : specif_scope. -Notation "[[[ x ]]]" := (inleft _ [x]) : specif_scope. +Notation "[|| x ||]" := (inleft _ [x]) : specif_scope. Notation "x <-- e1 ; e2" := (match e1 with | inright _ => !!