-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
-
+let nat_URI () =
+ try Some (List.hd !nat_URIs_ref) with Failure "hd" -> None
+let is_nat_URI uri =
+ List.exists (fun nat -> UriManager.eq nat uri) !nat_URIs_ref