new instantiate, only known bug is w.r.t. in/out scope and file matita/contribs/ng_as...

[helm.git] / helm / software / matita / contribs / ng_assembly / common / list_utility.ma

diff --git a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
index 3ffd1d3c5df48cd6f91116570aa2b1f7cc3c45ca..1c062a91297894d71284e594a553aa880a0c82e7 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -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 ≝
@@ -321,8 +321,6 @@ ndefinition abs_neList_aux1 : ∀T:Type.∀h:T.∀n.((len_neList T («£h»)) >
 ndefinition abs_neList_aux2 : ∀T:Type.∀h:T.∀t:ne_list T.∀n.((len_neList T (h§§t)) > (S n) = true) → ((len_neList T t) > n) = true.
  #T; #h; #t; #n; nnormalize; #H; napply H. nqed.
 
-naxiom daemon : False.
-
 nlet rec abs_neList (T:Type) (l:ne_list T) on l ≝
  match l
   return λl.Πn.(((len_neList T l) > n) = true) → T