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 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