Why does the Idris Nat data type start with 0, not 1?

Question

General Idris novelty question, sorry.

I was taught at school, there are natural numbers (N) and natural numbers with zero (N0).
In Idris, there is a data type Nat, which by definition corresponds to N0.

What will change if Nat is defined as follows:

data Nat = One | S Nat
data Nat0 = Zero | Nat

I think now it’s easier, but basically it is a problem with the implementation of the compiler or formal?

There should be cases where 0 does not make sense, and I think it is more difficult to determine correctly now. Or not?

Answer 1

, , , , , , . . , , .

, Nat, .

, , , . ( ), , , , , :

data Tree : Nat -> Type -> Type where
     Leaf : ty -> Tree 1 ty
     Node : Tree n ty -> Tree m ty -> Tree (n + m) ty

, , , Tree 0 Int, Tree 1 Int Tree 2 Int Tree n Int n > 0..

test1 : Tree 1 Int
test1 = Leaf 94

test2 : Tree 2 Int
test2 = Node test1 test1

test3 : Tree 3 Int
test3 = Node test1 test2

test0 : Tree 0 Int
test0 = ?no_chance