ground_2 milestone: multiple relocation with lists of booleans

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / lib / list.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma
index 9355f9c56185175fa263fba844548e432a7672f9..e72b54531a68816777ebcab50614b146f8c87bbe 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma
@@ -28,6 +28,14 @@ interpretation "nil (list)" 'Nil = (nil ?).
 
 interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl).
 
+let rec length (A:Type[0]) (l:list A) on l ≝ match l with
+[ nil      ⇒ 0
+| cons _ l ⇒ length A l + 1
+].
+
+interpretation "length (list)"
+   'card l = (length ? l).
+
 let rec all A (R:predicate A) (l:list A) on l ≝
   match l with
   [ nil        ⇒ ⊤