diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-16 14:50:35 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-16 14:50:35 +0000 |
| commit | a4deb2c27bdbbba5053c0b25a326ee24a2f42e1a (patch) | |
| tree | 29c8c169e287fdffd89a2f88d5628230ca8c952f /theories/Program/Syntax.v | |
| parent | a76ad2ccdc57f54bd23e1c64f3f4a4af8e912050 (diff) | |
Misc: Add test for bug 1704, now closed. Add usual syntax for lists in
Program.Syntax along with stronger implicits. Update dependent induction
test file using unicode syntax.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10682 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Program/Syntax.v')
| -rw-r--r-- | theories/Program/Syntax.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index ecdacce64..dd8536d57 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -35,6 +35,17 @@ Implicit Arguments inr [[A] [B]]. Implicit Arguments left [[A] [B]]. Implicit Arguments right [[A] [B]]. +Require Import Coq.Lists.List. + +Implicit Arguments nil [[A]]. +Implicit Arguments cons [[A]]. + +(** Standard notations for lists. *) + +Notation " [] " := nil. +Notation " [ x ] " := (cons x nil). +Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..). + (** n-ary exists ! *) Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p)))) |