Mercurial > cpdt > repo

comparison src/MoreSpecif.v @ 86:fd505bcb5632

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of certified regexp matcher
author Adam Chlipala <adamc@hcoop.net>
date Mon, 06 Oct 2008 14:33:11 -0400
parents 6c2607211cee
children 939add5a7db9
comparison
equal deleted inserted replaced
85:3746a2ded8da 86:fd505bcb5632
22 22
23 Notation "'Yes'" := (left _ _) : specif_scope. 23 Notation "'Yes'" := (left _ _) : specif_scope.
24 Notation "'No'" := (right _ _) : specif_scope. 24 Notation "'No'" := (right _ _) : specif_scope.
25 Notation "'Reduce' x" := (if x then Yes else No) (at level 50) : specif_scope. 25 Notation "'Reduce' x" := (if x then Yes else No) (at level 50) : specif_scope.
26 26
27 Notation "x || y" := (if x then Yes else Reduce y) (at level 50) : specif_scope. 27 Notation "x || y" := (if x then Yes else Reduce y) (at level 50, left associativity) : specif_scope.
28
29 Section sumbool_and.
30 Variables P1 Q1 P2 Q2 : Prop.
31
32 Variable x1 : {P1} + {Q1}.
33 Variable x2 : {P2} + {Q2}.
34
35 Definition sumbool_and : {P1 /\ P2} + {Q1 \/ Q2} :=
36 match x1 with
37 | left HP1 =>
38 match x2 with
39 | left HP2 => left _ (conj HP1 HP2)
40 | right HQ2 => right _ (or_intror _ HQ2)
41 end
42 | right HQ1 => right _ (or_introl _ HQ1)
43 end.
44 End sumbool_and.
45
46 Infix "&&" := sumbool_and (at level 40, left associativity) : specif_scope.
28 47
29 Inductive maybe (A : Type) (P : A -> Prop) : Set := 48 Inductive maybe (A : Type) (P : A -> Prop) : Set :=
30 | Unknown : maybe P 49 | Unknown : maybe P
31 | Found : forall x : A, P x -> maybe P. 50 | Found : forall x : A, P x -> maybe P.
32 51