-let destroy_nat =
- let is_nat_URI = NUri.eq (NUri.uri_of_string
- "cic:/matita/ng/arithmetics/nat/nat.ind") in
- let is_zero = function
- | NCic.Const (NReference.Ref (uri, NReference.Con (0, 1, 0))) when
- is_nat_URI uri -> true
- | _ -> false
- in
- let is_succ = function
- | NCic.Const (NReference.Ref (uri, NReference.Con (0, 2, 0))) when
- is_nat_URI uri -> true
- | _ -> false
- in
- let rec aux acc = function
- | NCic.Appl [he ; tl] when is_succ he -> aux (acc + 1) tl
- | t when is_zero t -> Some acc
- | _ -> None
- in
- aux 0
-