matita/matita/nlibrary/datatypes/list.ma

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