Mercurial > cpdt > repo
comparison src/MoreSpecif.v @ 86:fd505bcb5632
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 |