adamc@78: (* Copyright (c) 2008, Adam Chlipala adamc@78: * adamc@78: * This work is licensed under a adamc@78: * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 adamc@78: * Unported License. adamc@78: * The license text is available at: adamc@78: * http://creativecommons.org/licenses/by-nc-nd/3.0/ adamc@78: *) adamc@78: adamc@78: (* Types and notations presented in Chapter 6 *) adamc@78: adamc@78: Set Implicit Arguments. adamc@78: adamc@78: adamc@78: Notation "!" := (False_rec _ _) : specif_scope. adamc@78: Notation "[ e ]" := (exist _ e _) : specif_scope. adamc@78: Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2) adamc@78: (right associativity, at level 60) : specif_scope. adamc@78: adamc@78: Open Local Scope specif_scope. adamc@78: Delimit Scope specif_scope with specif. adamc@78: adamc@78: Notation "'Yes'" := (left _ _) : specif_scope. adamc@78: Notation "'No'" := (right _ _) : specif_scope. adamc@78: Notation "'Reduce' x" := (if x then Yes else No) (at level 50) : specif_scope. adamc@78: adamc@78: Notation "x || y" := (if x then Yes else Reduce y) (at level 50) : specif_scope. adamc@78: adamc@78: Inductive maybe (A : Type) (P : A -> Prop) : Set := adamc@78: | Unknown : maybe P adamc@78: | Found : forall x : A, P x -> maybe P. adamc@78: adamc@78: Notation "{{ x | P }}" := (maybe (fun x => P)) : specif_scope. adamc@78: Notation "??" := (Unknown _) : specif_scope. adamc@78: Notation "[[ x ]]" := (Found _ x _) : specif_scope. adamc@78: adamc@78: Notation "x <- e1 ; e2" := (match e1 with adamc@78: | Unknown => ?? adamc@78: | Found x _ => e2 adamc@78: end) adamc@78: (right associativity, at level 60) : specif_scope. adamc@78: adamc@79: Notation "!!" := (inright _ _) : specif_scope. adamc@79: Notation "[[[ x ]]]" := (inleft _ [x]) : specif_scope. adamc@79: adamc@78: Notation "x <-- e1 ; e2" := (match e1 with adamc@78: | inright _ => !! adamc@78: | inleft (exist x _) => e2 adamc@78: end) adamc@78: (right associativity, at level 60) : specif_scope. adamc@78: adamc@78: Notation "e1 ;; e2" := (if e1 then e2 else ??) adamc@78: (right associativity, at level 60) : specif_scope. adamc@78: adamc@78: Notation "e1 ;;; e2" := (if e1 then e2 else !!) adamc@78: (right associativity, at level 60) : specif_scope.