(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
(* 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