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 "list/list.ma".
17 interpretation "list nth" 'nth = (nth _).
18 interpretation "list nth" 'nth_appl l d i = (nth _ l d i).
19 notation "'nth'" with precedence 90 for @{'nth}.
20 notation < "'nth' \nbsp term 90 l \nbsp term 90 d \nbsp term 90 i"
21 with precedence 69 for @{'nth_appl $l $d $i}.
23 definition make_list ≝
25 let rec make_list (n:nat) on n ≝
26 match n with [ O ⇒ nil ? | S m ⇒ def m :: make_list m]
29 interpretation "'mk_list' appl" 'mk_list_appl f n = (make_list _ f n).
30 interpretation "'mk_list'" 'mk_list = (make_list _).
31 notation "'mk_list'" with precedence 90 for @{'mk_list}.
32 notation < "'mk_list' \nbsp term 90 f \nbsp term 90 n"
33 with precedence 69 for @{'mk_list_appl $f $n}.
35 notation "'len'" with precedence 90 for @{'len}.
36 interpretation "len" 'len = (length _).
37 notation < "'len' \nbsp term 90 l" with precedence 69 for @{'len_appl $l}.
38 interpretation "len appl" 'len_appl l = (length _ l).
40 lemma len_mk_list : ∀T:Type.∀f:nat→T.∀n.len (mk_list f n) = n.
41 intros; elim n; [reflexivity] simplify; rewrite > H; reflexivity;