annotate src/MoreSpecif.v @ 534:ed829eaa91b2

Builds with Coq 8.5beta2
author Adam Chlipala Wed, 05 Aug 2015 14:46:55 -0400 3322367e955d
rev   line source
adam@353 10 (* Types and notations presented in Chapter 6 *)
adamc@78 16 Notation "!" := (False_rec _ _) : specif_scope.
adamc@78 17 Notation "[ e ]" := (exist _ e _) : specif_scope.
adamc@78 18 Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2)
adamc@78 19 (right associativity, at level 60) : specif_scope.
adamc@221 21 Local Open Scope specif_scope.
adamc@78 22 Delimit Scope specif_scope with specif.
adamc@78 24 Notation "'Yes'" := (left _ _) : specif_scope.
adamc@78 25 Notation "'No'" := (right _ _) : specif_scope.
adamc@78 26 Notation "'Reduce' x" := (if x then Yes else No) (at level 50) : specif_scope.
adamc@86 28 Notation "x || y" := (if x then Yes else Reduce y) (at level 50, left associativity) : specif_scope.
adamc@86 31 Variables P1 Q1 P2 Q2 : Prop.
adamc@86 33 Variable x1 : {P1} + {Q1}.
adamc@86 34 Variable x2 : {P2} + {Q2}.
adamc@86 36 Definition sumbool_and : {P1 /\ P2} + {Q1 \/ Q2} :=
adamc@86 38 | left HP1 =>
adamc@86 40 | left HP2 => left _ (conj HP1 HP2)
adamc@86 41 | right HQ2 => right _ (or_intror _ HQ2)
adamc@86 43 | right HQ1 => right _ (or_introl _ HQ1)
adamc@86 47 Infix "&&" := sumbool_and (at level 40, left associativity) : specif_scope.
adamc@89 49 Inductive maybe (A : Set) (P : A -> Prop) : Set :=
adamc@78 50 | Unknown : maybe P
adamc@78 51 | Found : forall x : A, P x -> maybe P.
adamc@78 53 Notation "{{ x | P }}" := (maybe (fun x => P)) : specif_scope.
adamc@78 54 Notation "??" := (Unknown _) : specif_scope.
adam@335 55 Notation "[| x |]" := (Found _ x _) : specif_scope.
adamc@78 57 Notation "x <- e1 ; e2" := (match e1 with
adamc@78 58 | Unknown => ??
adamc@78 59 | Found x _ => e2
adamc@78 61 (right associativity, at level 60) : specif_scope.
adamc@79 63 Notation "!!" := (inright _ _) : specif_scope.
adam@335 64 Notation "[|| x ||]" := (inleft _ [x]) : specif_scope.
adamc@78 66 Notation "x <-- e1 ; e2" := (match e1 with
adamc@78 67 | inright _ => !!
adamc@78 68 | inleft (exist x _) => e2
adamc@78 70 (right associativity, at level 60) : specif_scope.
adamc@78 72 Notation "e1 ;; e2" := (if e1 then e2 else ??)
adamc@78 73 (right associativity, at level 60) : specif_scope.
adamc@78 75 Notation "e1 ;;; e2" := (if e1 then e2 else !!)
adamc@78 76 (right associativity, at level 60) : specif_scope.
adamc@142 80 Variable P : Prop.
adamc@142 82 Inductive partial : Set :=
adamc@142 83 | Proved : P -> partial
adamc@142 84 | Uncertain : partial.