annotate src/MoreSpecif.v @ 82:15e2b3485dc4

Subset exercises
author Adam Chlipala <adamc@hcoop.net>
date Sun, 05 Oct 2008 12:12:19 -0400
parents 6c2607211cee
children fd505bcb5632
rev   line source
adamc@78 1 (* Copyright (c) 2008, Adam Chlipala
adamc@78 2 *
adamc@78 3 * This work is licensed under a
adamc@78 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@78 5 * Unported License.
adamc@78 6 * The license text is available at:
adamc@78 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@78 8 *)
adamc@78 9
adamc@78 10 (* Types and notations presented in Chapter 6 *)
adamc@78 11
adamc@78 12 Set Implicit Arguments.
adamc@78 13
adamc@78 14
adamc@78 15 Notation "!" := (False_rec _ _) : specif_scope.
adamc@78 16 Notation "[ e ]" := (exist _ e _) : specif_scope.
adamc@78 17 Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2)
adamc@78 18 (right associativity, at level 60) : specif_scope.
adamc@78 19
adamc@78 20 Open Local Scope specif_scope.
adamc@78 21 Delimit Scope specif_scope with specif.
adamc@78 22
adamc@78 23 Notation "'Yes'" := (left _ _) : specif_scope.
adamc@78 24 Notation "'No'" := (right _ _) : specif_scope.
adamc@78 25 Notation "'Reduce' x" := (if x then Yes else No) (at level 50) : specif_scope.
adamc@78 26
adamc@78 27 Notation "x || y" := (if x then Yes else Reduce y) (at level 50) : specif_scope.
adamc@78 28
adamc@78 29 Inductive maybe (A : Type) (P : A -> Prop) : Set :=
adamc@78 30 | Unknown : maybe P
adamc@78 31 | Found : forall x : A, P x -> maybe P.
adamc@78 32
adamc@78 33 Notation "{{ x | P }}" := (maybe (fun x => P)) : specif_scope.
adamc@78 34 Notation "??" := (Unknown _) : specif_scope.
adamc@78 35 Notation "[[ x ]]" := (Found _ x _) : specif_scope.
adamc@78 36
adamc@78 37 Notation "x <- e1 ; e2" := (match e1 with
adamc@78 38 | Unknown => ??
adamc@78 39 | Found x _ => e2
adamc@78 40 end)
adamc@78 41 (right associativity, at level 60) : specif_scope.
adamc@78 42
adamc@79 43 Notation "!!" := (inright _ _) : specif_scope.
adamc@79 44 Notation "[[[ x ]]]" := (inleft _ [x]) : specif_scope.
adamc@79 45
adamc@78 46 Notation "x <-- e1 ; e2" := (match e1 with
adamc@78 47 | inright _ => !!
adamc@78 48 | inleft (exist x _) => e2
adamc@78 49 end)
adamc@78 50 (right associativity, at level 60) : specif_scope.
adamc@78 51
adamc@78 52 Notation "e1 ;; e2" := (if e1 then e2 else ??)
adamc@78 53 (right associativity, at level 60) : specif_scope.
adamc@78 54
adamc@78 55 Notation "e1 ;;; e2" := (if e1 then e2 else !!)
adamc@78 56 (right associativity, at level 60) : specif_scope.