[Agda] Positive numbers

[Jim Burton]

At Tue, 3 Mar 2009 11:43:38 +0900,
Gyesik Lee wrote:
>

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

But then how could I pattern-match on the value of the pos in the body
of functions?
 
> 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 didn't know that, and thought the opposite. I will look (again) at
Ulf's tutorial.

Thanks,

Jim