Quick hack: matita natural numbers are now accepted by the parser/disambiguator.

[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 579c21eede3a9f2f2e44023d180377fcf2282341..e2f5fd36324ba017a59c6509f0b4bdf7f14f87a1 100644 (file)
--- a/helm/software/components/cic/libraryObjects.ml
+++ b/helm/software/components/cic/libraryObjects.ml
@@ -194,3 +194,16 @@ 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 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