[Agda] Positive numbers

[Gyesik Lee]

>> How about with the following one?
>>
>> data N+ : N -> Set where
>> pos : forall {n : N} -> N+ (succ n)

Sorry, this was probably not what you want.
I thought just so because N+ has a function type.

>> Since Agda provides non-exhaustive pattern-matching, I believe, you
>> don't need to worry about positiveness.
>> (Cf. Ulf Norell's "Dependently Typed Programming in Agda")

I meant with that you can use non-exhaustive pattern-matching when the
argument type apparently contains no zero.
I realize now that you were maybe talking of dependent types, I mean
numbers with positive condition (n > 0).