]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/ng_assembly/common/list_utility.ma
freescale porting, work in progress
[helm.git] / helm / software / matita / contribs / ng_assembly / common / list_utility.ma
index ae40ba75db0018b49faf3c0d02471d56dfe48071..ce118e74c11af46c24c08ef6efd7f9d7770d26a1 100755 (executable)
@@ -188,7 +188,7 @@ nlet rec abs_list (T:Type) (l:list T) on l ≝
 
 (* listlen *)
 nlet rec len_neList (T:Type) (nl:ne_list T) on nl ≝
- match nl with [ ne_nil _ ⇒ 1 | ne_cons _ t ⇒ S (len_neList T t) ].
+ match nl with [ ne_nil _ ⇒ (S O) | ne_cons _ t ⇒ S (len_neList T t) ].
 
 (* reverse *)
 nlet rec reverse_neList (T:Type) (nl:ne_list T) on nl ≝