Mercurial > cpdt > repo
diff 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 |
line wrap: on
line diff
--- a/src/MoreSpecif.v Mon Oct 06 13:07:24 2008 -0400 +++ b/src/MoreSpecif.v Mon Oct 06 14:33:11 2008 -0400 @@ -24,7 +24,26 @@ Notation "'No'" := (right _ _) : specif_scope. Notation "'Reduce' x" := (if x then Yes else No) (at level 50) : specif_scope. -Notation "x || y" := (if x then Yes else Reduce y) (at level 50) : specif_scope. +Notation "x || y" := (if x then Yes else Reduce y) (at level 50, left associativity) : specif_scope. + +Section sumbool_and. + Variables P1 Q1 P2 Q2 : Prop. + + Variable x1 : {P1} + {Q1}. + Variable x2 : {P2} + {Q2}. + + Definition sumbool_and : {P1 /\ P2} + {Q1 \/ Q2} := + match x1 with + | left HP1 => + match x2 with + | left HP2 => left _ (conj HP1 HP2) + | right HQ2 => right _ (or_intror _ HQ2) + end + | right HQ1 => right _ (or_introl _ HQ1) + end. +End sumbool_and. + +Infix "&&" := sumbool_and (at level 40, left associativity) : specif_scope. Inductive maybe (A : Type) (P : A -> Prop) : Set := | Unknown : maybe P