diff options
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 ecdacce64a..dd8536d572 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)))) |