X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FlibraryObjects.ml;h=7e1dc626f7885afe404fe224310b5c2a60a196e8;hb=468ee32f0fc7de271454ed94643b4dd7c9578e5f;hp=579c21eede3a9f2f2e44023d180377fcf2282341;hpb=ea651f11cbc6edb17e8d0d16c239e0cf3f526959;p=helm.git

diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml
index 579c21eed..7e1dc626f 100644
--- a/helm/software/components/cic/libraryObjects.ml
+++ b/helm/software/components/cic/libraryObjects.ml
@@ -194,3 +194,32 @@ let false_URI () =
  try Some (List.hd !false_URIs_ref) with Failure "hd" -> None
 let absurd_URI () =
  try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None
+
+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
+    | 0 -> zero
+    | 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
+