]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/common/list.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / ng_assembly / common / list.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "common/theory.ma".
24
25 (* *************** *)
26 (* LISTE GENERICHE *)
27 (* *************** *)
28
29 ninductive list (A:Type) : Type ≝
30   nil: list A
31 | cons: A → list A → list A.
32
33 nlet rec append A (l1: list A) l2 on l1 ≝
34  match l1 with
35   [ nil ⇒ l2
36   | (cons hd tl) ⇒ cons A hd (append A tl l2) ].
37
38 notation "hvbox(hd break :: tl)"
39   right associative with precedence 47
40   for @{'cons $hd $tl}.
41
42 notation "[ list0 x sep ; ]"
43   non associative with precedence 90
44   for ${fold right @'nil rec acc @{'cons $x $acc}}.
45
46 notation "hvbox(l1 break @ l2)"
47   right associative with precedence 47
48   for @{'append $l1 $l2 }.
49
50 interpretation "nil" 'nil = (nil ?).
51 interpretation "cons" 'cons hd tl = (cons ? hd tl).
52 interpretation "append" 'append l1 l2 = (append ? l1 l2).
53
54 (* ************** *)
55 (* NON-EMPTY LIST *)
56 (* ************** *)
57
58 (* lista non vuota *)
59 ninductive ne_list (A:Type) : Type ≝
60   | ne_nil: A → ne_list A
61   | ne_cons: A → ne_list A → ne_list A.
62
63 (* append *)
64 nlet rec ne_append (A:Type) (l1,l2:ne_list A) on l1 ≝
65  match l1 with
66   [ ne_nil hd ⇒ ne_cons A hd l2
67   | ne_cons hd tl ⇒ ne_cons A hd (ne_append A tl l2) ].
68
69 notation "hvbox(hd break §§ tl)"
70   right associative with precedence 46
71   for @{'ne_cons $hd $tl}.
72
73 (* \laquo \raquo *)
74 notation "« list0 x sep ; break £ y break »"
75   non associative with precedence 90
76   for ${fold right @{'ne_nil $y } rec acc @{'ne_cons $x $acc}}.
77
78 notation "hvbox(l1 break & l2)"
79   right associative with precedence 47
80   for @{'ne_append $l1 $l2 }.
81
82 interpretation "ne_nil" 'ne_nil hd = (ne_nil ? hd).
83 interpretation "ne_cons" 'ne_cons hd tl = (ne_cons ? hd tl).
84 interpretation "ne_append" 'ne_append l1 l2 = (ne_append ? l1 l2).