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/notation/constructors/nil_0.ma".
16 include "ground_2/notation/constructors/oplusright_5.ma".
17 include "ground_2/lib/arith.ma".
19 (* LISTS OF PAIRS ***********************************************************)
21 inductive list2 (A1,A2:Type[0]) : Type[0] :=
23 | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2.
25 interpretation "nil (list of pairs)" 'Nil = (nil2 ? ?).
27 interpretation "cons (list of pairs)"
28 'OPlusRight A1 A2 hd1 hd2 tl = (cons2 A1 A2 hd1 hd2 tl).
30 rec definition length2 A1 A2 (l:list2 A1 A2) on l ≝ match l with
32 | cons2 _ _ l ⇒ ↑(length2 A1 A2 l)
35 interpretation "length (list of pairs)"
36 'card l = (length2 ? ? l).