diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-26 15:58:32 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-26 15:58:32 +0000 |
| commit | d081dcfaedb5b7e2ad78574a053bcebc4bfb564a (patch) | |
| tree | dfdb78d703b6eb48d43b4ca555a3fd24e37db574 /theories/Program/Basics.v | |
| parent | e467f77a19229058070d43e9cf1080534b9aee74 (diff) | |
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
Diffstat (limited to 'theories/Program/Basics.v')
| -rw-r--r-- | theories/Program/Basics.v | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 3040dd04b..8a3e5dccd 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 *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -18,7 +19,7 @@ Unset Strict Implicit. Require Export Coq.Program.FunctionalExtensionality. -Notation "'λ' x : T , y" := (fun x:T => 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 |