diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 15:36:20 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-05 19:52:23 +0200 |
commit | 8e3c749e69649fb45750355e464ce7c16a4462c7 (patch) | |
tree | a7bc1a3bed029eab91366cf1dd9e0e53415a0e2a /theories | |
parent | 1fe47f95097b0245081a4feb4a5d44f761301dca (diff) |
Improving printing of "[]" (nil) in spite of the risk of collision
with possible further use of token "[]" + slight restructuration.
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Lists/List.v | 29 |
1 files changed, 14 insertions, 15 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 3e660caab..378cf722a 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -21,6 +21,16 @@ Set Implicit Arguments. Open Scope list_scope. +(** Standard notations for lists. +In a special module to avoid conflicts. *) +Module ListNotations. +Notation " [ ] " := nil (format "[ ]") : list_scope. +Notation " [ x ] " := (cons x nil) : list_scope. +Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. +End ListNotations. + +Import ListNotations. + Section Lists. Variable A : Type. @@ -29,42 +39,31 @@ Section Lists. Definition hd (default:A) (l:list A) := match l with - | nil => default + | [] => default | x :: _ => x end. Definition hd_error (l:list A) := match l with - | nil => error + | [] => error | x :: _ => value x end. Definition tl (l:list A) := match l with - | nil => nil + | [] => nil | a :: m => m end. (** The [In] predicate *) Fixpoint In (a:A) (l:list A) : Prop := match l with - | nil => False + | [] => False | b :: m => b = a \/ In a m end. End Lists. - -(** Standard notations for lists. -In a special module to avoid conflict. *) -Module ListNotations. -Notation " [ ] " := nil : list_scope. -Notation " [ x ] " := (cons x nil) : list_scope. -Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. -End ListNotations. - -Import ListNotations. - Section Facts. Variable A : Type. |