Added in basics

[helm.git] / matita / matita / lib / basics / lists / listb.ma

diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma
index 5abf50f14274a39f3330ff7da75995a8bce0f8e4..b6d5864f8c0a14cd2db42bc786f1c1651e7e966d 100644 (file)
--- a/matita/matita/lib/basics/lists/listb.ma
+++ b/matita/matita/lib/basics/lists/listb.ma
@@ -16,6 +16,13 @@ include "basics/lists/list.ma".
 include "basics/sets.ma".
 include "basics/deqsets.ma".
 
+(********* isnilb *********)
+let rec isnilb A (l: list A) on l ≝
+match l with
+[ nil ⇒ true
+| cons hd tl ⇒ false
+].
+
 (********* search *********)
 
 let rec memb (S:DeqSet) (x:S) (l: list S) on l  ≝