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