V_______________________________________________________________ *)
include "basics/types.ma".
-include "basics/bool.ma".
+include "arithmetics/nat.ma".
inductive list (A:Type[0]) : Type[0] :=
| nil: list A
| cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
].
+(**************************** length ******************************)
+
+let rec length (A:Type[0]) (l:list A) on l ≝
+ match l with
+ [ nil ⇒ 0
+ | cons a tl ⇒ S (length A tl)].
+
+notation "|M|" non associative with precedence 60 for @{'norm $M}.
+interpretation "norm" 'norm l = (length ? l).
+
+let rec nth n (A:Type[0]) (l:list A) (d:A) ≝
+ match n with
+ [O ⇒ hd A l d
+ |S m ⇒ nth m A (tail A l) d].
+
(**************************** fold *******************************)
let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝