# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223063999 14400
# Node ID c49d999fe8066dabf0d1cc91a73a95c38019e375
# Parent  d07c77659c2073c055c870733ed4fb2351966e04
MoreSpecif

diff -r d07c77659c20 -r c49d999fe806 Makefile
--- 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)
diff -r d07c77659c20 -r c49d999fe806 src/MoreSpecif.v
--- /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.