]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/ng_assembly/common/nat.ma
freescale porting, work in progress
[helm.git] / helm / software / matita / contribs / ng_assembly / common / nat.ma
index 4db935b1e1698e1edc514d2926e5f1e6d1ab3a7a..9188bef9edb808b057ec00d08a563477d98124b9 100755 (executable)
@@ -26,15 +26,17 @@ include "num/bool.ma".
 (* NATURALI *)
 (* ******** *)
 
-inductive nat : Type ≝
+ninductive nat : Type ≝
   O : nat
 | S : nat → nat.
 
+(*
 interpretation "Natural numbers" 'N = nat.
 
 default "natural numbers" cic:/matita/common/nat/nat.ind.
 
 alias num (instance 0) = "natural number".
+*)
 
 nlet rec eq_nat (n1,n2:nat) on n1 ≝
  match n1 with