X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Futility.ma;h=94adb3caf0d4d7a3385955438e2058602f055bb0;hb=c22f39a5d5afc0ef55beb221e00e2e6703b13d90;hp=c67298d390673fe02d0519d1241ed2e84a389133;hpb=55e5bef77f163b29feeb9ad4e83376c5aa301297;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/compiler/utility.ma b/helm/software/matita/contribs/assembly/compiler/utility.ma
index c67298d39..94adb3caf 100755
--- a/helm/software/matita/contribs/assembly/compiler/utility.ma
+++ b/helm/software/matita/contribs/assembly/compiler/utility.ma
@@ -48,9 +48,9 @@ notation "hvbox(l1 break & l2)"
   right associative with precedence 47
   for @{'ne_append $l1 $l2 }.
 
-interpretation "ne_nil" 'ne_nil hd = (ne_nil _ hd).
-interpretation "ne_cons" 'ne_cons hd tl = (ne_cons _ hd tl).
-interpretation "ne_append" 'ne_append l1 l2 = (ne_append _ l1 l2).
+interpretation "ne_nil" 'ne_nil hd = (ne_nil ? hd).
+interpretation "ne_cons" 'ne_cons hd tl = (ne_cons ? hd tl).
+interpretation "ne_append" 'ne_append l1 l2 = (ne_append ? l1 l2).
 
 (* ************ *)
 (* List Utility *)
@@ -198,6 +198,21 @@ lemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empt
    normalize; autobatch ]
 qed.
 
+definition isnot_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ False | cons _ _ ⇒ True ].
+
+definition isnotb_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ false | cons _ _ ⇒ true ].
+
+lemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
+ unfold isnotb_empty_list;
+ unfold isnot_empty_list;
+ intros;
+ elim l;
+ [ normalize; autobatch |
+   normalize; autobatch ]
+qed.
+
 lemma isempty_to_eq : ∀T,l.isb_empty_list T l = true → l = [].
  do 2 intro;
  elim l 0;