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 *)
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;