Mercurial > cpdt > repo

comparison 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
comparison
equal deleted inserted replaced
78:c49d999fe806 79:6c2607211cee
38 | Unknown => ?? 38 | Unknown => ??
39 | Found x _ => e2 39 | Found x _ => e2
40 end) 40 end)
41 (right associativity, at level 60) : specif_scope. 41 (right associativity, at level 60) : specif_scope.
42 42
43 Notation "!!" := (inright _ _) : specif_scope.
44 Notation "[[[ x ]]]" := (inleft _ [x]) : specif_scope.
45
43 Notation "x <-- e1 ; e2" := (match e1 with 46 Notation "x <-- e1 ; e2" := (match e1 with
44 | inright _ => !! 47 | inright _ => !!
45 | inleft (exist x _) => e2 48 | inleft (exist x _) => e2
46 end) 49 end)
47 (right associativity, at level 60) : specif_scope. 50 (right associativity, at level 60) : specif_scope.