From a76ad2ccdc57f54bd23e1c64f3f4a4af8e912050 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 16 Mar 2008 13:40:45 +0000
Subject: Reorganize Program and Classes theories. Requiring Setoid no longer
 sets implicits for left, inl or eq, hence some theories had to be changed
 again. It should make some user contribs compile again too. Also do not
 import functional extensionality when importing Program.Basics, add a
 Combinators file for proofs requiring it and a Syntax file for the implicit
 settings. Move Classes.Relations to Classes.RelationClasses to avoid name
 clash warnings as advised by Hugo and Pierre.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10681 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Syntax.v | 58 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 58 insertions(+)
 create mode 100644 theories/Program/Syntax.v

(limited to 'theories/Program/Syntax.v')

diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
new file mode 100644
index 0000000000..ecdacce64a
--- /dev/null
+++ b/theories/Program/Syntax.v
@@ -0,0 +1,58 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Custom notations and implicits for Coq prelude definitions.
+ *
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+ *              91405 Orsay, France *)
+
+(** Unicode lambda abstraction, does not work with factorization of lambdas. *)
+
+Notation  " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T,y at level 10, no associativity) : program_scope.
+
+(** Notations for the unit type and value. *)
+
+Notation " () " := Datatypes.unit : type_scope.
+Notation " () " := tt.
+
+(** Set maximally inserted implicit arguments for standard definitions. *)
+
+Implicit Arguments eq [[A]].
+
+Implicit Arguments Some [[A]].
+Implicit Arguments None [[A]].
+
+Implicit Arguments inl [[A] [B]].
+Implicit Arguments inr [[A] [B]].
+
+Implicit Arguments left [[A] [B]].
+Implicit Arguments right [[A] [B]].
+
+(** n-ary exists ! *)
+
+Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p))))
+  (at level 200, x ident, y ident, right associativity) : type_scope.
+
+Notation " 'exists' x y z , p" := (ex (fun x => (ex (fun y => (ex (fun z => p))))))
+  (at level 200, x ident, y ident, z ident, right associativity) : type_scope.
+
+Notation " 'exists' x y z w , p" := (ex (fun x => (ex (fun y => (ex (fun z => (ex (fun w => p))))))))
+  (at level 200, x ident, y ident, z ident, w ident, right associativity) : type_scope.
+
+Tactic Notation "exist" constr(x) := exists x.
+Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y.
+Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
+Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
+
+(* Notation " 'Σ' x : T , p" := (sigT (fun x : T => p)) *)
+(*   (at level 200, x ident, y ident, right associativity) : program_scope. *)
+
+(* Notation " 'Π' x : T , p " := (forall x : T, p) *)
+(*   (at level 200, x ident, right associativity) : program_scope. *)
\ No newline at end of file
-- 
cgit v1.2.3