Dirty patch by Zack: natural numbers of Matita are now pretty-printed as numbers...

[helm.git] / helm / software / components / cic / libraryObjects.ml

diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml
index e2f5fd36324ba017a59c6509f0b4bdf7f14f87a1..7e1dc626f7885afe404fe224310b5c2a60a196e8 100644 (file)
--- 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
+