Mercurial > cpdt > repo

comparison src/MoreSpecif.v @ 335:1f57a8d0ed3d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass over Subset
author Adam Chlipala <adam@chlipala.net>
date Wed, 05 Oct 2011 11:32:13 -0400
parents 54e8ecb5ec88
children ad315efc3b6b
comparison
equal deleted inserted replaced
334:386b7ad8849b 335:1f57a8d0ed3d
1 (* Copyright (c) 2008, Adam Chlipala 1 (* Copyright (c) 2008, 2011, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
49 | Unknown : maybe P 49 | Unknown : maybe P
50 | Found : forall x : A, P x -> maybe P. 50 | Found : forall x : A, P x -> maybe P.
51 51
52 Notation "{{ x | P }}" := (maybe (fun x => P)) : specif_scope. 52 Notation "{{ x | P }}" := (maybe (fun x => P)) : specif_scope.
53 Notation "??" := (Unknown _) : specif_scope. 53 Notation "??" := (Unknown _) : specif_scope.
54 Notation "[[ x ]]" := (Found _ x _) : specif_scope. 54 Notation "[| x |]" := (Found _ x _) : specif_scope.
55 55
56 Notation "x <- e1 ; e2" := (match e1 with 56 Notation "x <- e1 ; e2" := (match e1 with
57 | Unknown => ?? 57 | Unknown => ??
58 | Found x _ => e2 58 | Found x _ => e2
59 end) 59 end)
60 (right associativity, at level 60) : specif_scope. 60 (right associativity, at level 60) : specif_scope.
61 61
62 Notation "!!" := (inright _ _) : specif_scope. 62 Notation "!!" := (inright _ _) : specif_scope.
63 Notation "[[[ x ]]]" := (inleft _ [x]) : specif_scope. 63 Notation "[|| x ||]" := (inleft _ [x]) : specif_scope.
64 64
65 Notation "x <-- e1 ; e2" := (match e1 with 65 Notation "x <-- e1 ; e2" := (match e1 with
66 | inright _ => !! 66 | inright _ => !!
67 | inleft (exist x _) => e2 67 | inleft (exist x _) => e2
68 end) 68 end)