1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "logic/pts.ma".
17 ninductive list (A:Type[0]) : Type[0] ≝
19 | cons: A -> list A -> list A.
21 notation "hvbox(hd break :: tl)"
22 right associative with precedence 47
25 notation "[ list0 x sep ; ]"
26 non associative with precedence 90
27 for ${fold right @'nil rec acc @{'cons $x $acc}}.
29 notation "hvbox(l1 break @ l2)"
30 right associative with precedence 47
31 for @{'append $l1 $l2 }.
33 interpretation "nil" 'nil = (nil ?).
34 interpretation "cons" 'cons hd tl = (cons ? hd tl).
36 nlet rec append A (l1: list A) l2 on l1 ≝
39 | cons hd tl ⇒ hd :: append A tl l2 ].
41 interpretation "append" 'append l1 l2 = (append ? l1 l2).
43 nlet rec id_list A (l: list A) on l ≝
46 | cons hd tl ⇒ hd :: id_list A tl ].
49 ndefinition tail ≝ λA:Type[0].λl:list A.
54 nlet rec flatten S (l : list (list S)) on l : list S ≝
55 match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].