X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FlibraryObjects.ml;h=7e1dc626f7885afe404fe224310b5c2a60a196e8;hb=bb0074a578a1d4860516964a3717a99a70c0f28c;hp=e2f5fd36324ba017a59c6509f0b4bdf7f14f87a1;hpb=6e61c5884aa89838a04659f90dc8d210e3703502;p=helm.git

diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml
index e2f5fd363..7e1dc626f 100644
--- a/helm/software/components/cic/libraryObjects.ml
+++ b/helm/software/components/cic/libraryObjects.ml
@@ -200,6 +200,14 @@ let nat_URI = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind"
 let zero = Cic.MutConstruct (nat_URI,0,1,[])
 let succ = Cic.MutConstruct (nat_URI,0,2,[])
 
+let is_zero = function
+  | Cic.AMutConstruct (_, uri, 0, 1, _) when UriManager.eq uri nat_URI -> true
+  | _ -> false
+
+let is_succ = function
+  | Cic.AMutConstruct (_, uri, 0, 2, _) when UriManager.eq uri nat_URI -> true
+  | _ -> false
+
 let build_nat n =
   if n < 0 then assert false;
   let rec aux = function
@@ -207,3 +215,11 @@ let build_nat n =
     | n -> Cic.Appl [ succ; (aux (n - 1)) ]
   in
   aux n
+
+let destroy_nat annterm =
+  let rec aux acc = function
+    | Cic.AAppl (_, [he ; tl]) when is_succ he -> aux (acc + 1) tl
+    | t when is_zero t -> Some acc
+    | _ -> None in
+  aux 0 annterm
+