[Agda] Positive numbers

[Nils Anders Danielsson]

On 2009-03-03 09:06, Jim Burton wrote:
> At Tue, 3 Mar 2009 11:43:38 +0900,
> Gyesik Lee wrote:
>  
>> 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?

f (pos {...}) = ...
f (pos {n = ...}) = ...

>> Since Agda provides non-exhaustive pattern-matching

> I didn't know that, and thought the opposite.

Agda should only accept exhaustive pattern-matching (if not, then please
report this as a bug). I think Gyesik referred to the fact that you do
not always need to match on all constructors of an inductive family.

-- 
/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.