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 "Ground_2/arith.ma".
17 (* LISTS ********************************************************************)
19 inductive list (A:Type[0]) : Type[0] :=
21 | cons: A → list A → list A.
23 interpretation "nil (list)" 'Nil = (nil ?).
25 interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl).
27 let rec all A (R:predicate A) (l:list A) on l ≝
30 | cons hd tl ⇒ R hd ∧ all A R tl
33 inductive list2 (A1,A2:Type[0]) : Type[0] :=
35 | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2.
37 interpretation "nil (list of pairs)" 'Nil2 = (nil2 ? ?). (**) (* 'Nil causes unification error in aacr_abst *)
39 interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl).
41 let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
43 | cons2 a1 a2 tl ⇒ {a1, a2} :: append2 A1 A2 tl l2
46 interpretation "append (list of pairs)"
47 'Append l1 l2 = (append2 ? ? l1 l2).
49 let rec length2 (A1,A2:Type[0]) (l:list2 A1 A2) on l ≝ match l with
51 | cons2 _ _ l ⇒ length2 A1 A2 l + 1
54 interpretation "length (list of pairs)"
55 'card l = (length2 ? ? l).