[Agda] Positive numbers

[Jim Burton]

At Mon, 02 Mar 2009 19:49:58 +0000,
Nils Anders Danielsson wrote:
> 
> On 2009-03-02 18:04, J.Burton at brighton.ac.uk wrote:
> > data N : Set where
> >   zero : N
> >   succ : N -> N
> > 
> > data N+ : N -> Set where
> >   pos : forall {n : N} -> (succ n) -> N+
> 
> The problem is that succ n is not a type.
>

Thanks Nils. My toy example was to avoid dividing by zero, so with
your hint I have


data 0< : N -> Set where
  is-succ : forall {n : N} -> 0< (succ n)

data N+ : Set where
  -- pos : {n : N} {is-succ : 0< n} -> (n : N) -> N+ -- allows pos zero
  -- pos : (n : N) -> {is-succ : 0< n} -> N+ -- allows pos zero
  pos : (n : N) -> (is-succ : 0< n) -> N+

_div_ : ℕ -> ℕ⁺ -> ℕ 
zero div m     = zero
n div (pos m p) with n < m
... | true  = zero
... | false = one + ((n - m) div (pos m p))
 
So I have to make values of N+ with (pos n is-succ). I would like the
is-succ argument to be implicit, as it must be redundant, but doing
that allows (pos zero). How can I fix that? Also, where should I look
to find the neater, idiomatic, more general etc ways of stating this
simple property?

Incidentally, emacs highlights _div_ and  div in the above in salmon pink
whereas other functions are in dark blue -- is there something special
about it? 

Regards,

Jim


> -- 
> /NAD
> 
> This message has been checked for viruses but the contents of an attachment
> may still contain software viruses, which could damage your computer system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.
>