]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic/libraryObjects.mli
- libraryObjects: new default "natural numbers" with the uri of nat.
[helm.git] / helm / software / components / cic / libraryObjects.mli
index b4e19dff80452402f04c92609563d4195c630a58..2488930024534141b4b4bb401517b2367dd2820c 100644 (file)
@@ -66,6 +66,5 @@ val false_URI : unit -> UriManager.uri option
 val true_URI : unit -> UriManager.uri option
 val absurd_URI : unit -> UriManager.uri option
 
-val build_nat : int -> Cic.term
-val destroy_nat : Cic.annterm -> int option
-
+val nat_URI : unit -> UriManager.uri option
+val is_nat_URI : UriManager.uri -> bool