Mercurial > cpdt > repo
changeset 78:c49d999fe806
MoreSpecif
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 03 Oct 2008 15:59:59 -0400 |
parents | d07c77659c20 |
children | 6c2607211cee |
files | Makefile src/MoreSpecif.v |
diffstat | 2 files changed, 54 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/Makefile Fri Oct 03 15:27:39 2008 -0400 +++ b/Makefile Fri Oct 03 15:59:59 2008 -0400 @@ -1,4 +1,4 @@ -MODULES_NODOC := Tactics +MODULES_NODOC := Tactics MoreSpecif MODULES_PROSE := Intro MODULES_CODE := StackMachine InductiveTypes Predicates Coinductive Subset MODULES_DOC := $(MODULES_PROSE) $(MODULES_CODE)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/MoreSpecif.v Fri Oct 03 15:59:59 2008 -0400 @@ -0,0 +1,53 @@ +(* Copyright (c) 2008, Adam Chlipala + * + * This work is licensed under a + * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 + * Unported License. + * The license text is available at: + * http://creativecommons.org/licenses/by-nc-nd/3.0/ + *) + +(* Types and notations presented in Chapter 6 *) + +Set Implicit Arguments. + + +Notation "!" := (False_rec _ _) : specif_scope. +Notation "[ e ]" := (exist _ e _) : specif_scope. +Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2) +(right associativity, at level 60) : specif_scope. + +Open Local Scope specif_scope. +Delimit Scope specif_scope with specif. + +Notation "'Yes'" := (left _ _) : specif_scope. +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. + +Inductive maybe (A : Type) (P : A -> Prop) : Set := +| Unknown : maybe P +| Found : forall x : A, P x -> maybe P. + +Notation "{{ x | P }}" := (maybe (fun x => P)) : specif_scope. +Notation "??" := (Unknown _) : specif_scope. +Notation "[[ x ]]" := (Found _ x _) : specif_scope. + +Notation "x <- e1 ; e2" := (match e1 with + | Unknown => ?? + | Found x _ => e2 + end) +(right associativity, at level 60) : specif_scope. + +Notation "x <-- e1 ; e2" := (match e1 with + | inright _ => !! + | inleft (exist x _) => e2 + end) +(right associativity, at level 60) : specif_scope. + +Notation "e1 ;; e2" := (if e1 then e2 else ??) + (right associativity, at level 60) : specif_scope. + +Notation "e1 ;;; e2" := (if e1 then e2 else !!) + (right associativity, at level 60) : specif_scope.