From d081dcfaedb5b7e2ad78574a053bcebc4bfb564a Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 26 Feb 2008 15:58:32 +0000 Subject: Proper implicit arguments handling for assumptions (Axiom/Variable...). New tactic clapply to apply unapplied class methods in tactic mode, simple solution to the fact that apply does not work up-to classes yet. Add Functions.v for class definitions related to functional morphisms. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10589 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Program/Basics.v | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'theories/Program/Basics.v') diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 3040dd04ba..8a3e5dccd9 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -1,3 +1,4 @@ +(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* y) (at level 1, x,T,y at level 10) : program_scope. +Notation " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T,y at level 10, no associativity) : program_scope. Open Scope program_scope. @@ -45,7 +46,7 @@ Proof. Qed. Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), - h ∘ (g ∘ f) = h ∘ g ∘ f. + h ∘ g ∘ f = h ∘ (g ∘ f). Proof. intros. reflexivity. @@ -117,7 +118,7 @@ Qed. (** Useful implicits and notations for lists. *) -Require Export Coq.Lists.List. +Require Import Coq.Lists.List. Implicit Arguments nil [[A]]. Implicit Arguments cons [[A]]. @@ -141,3 +142,9 @@ 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