[Agda] Positivity checker

[Wouter Swierstra]

On 8 Dec 2008, at 09:10, Nils Anders Danielsson wrote:
>>>
>>> Yes.
>> Why?

Another important reason for preferring data over functions into set  
is that Agda's pattern matching on data types is really quite clever.  
If you have what Conor calls "catholic" data types such as:

data Leq : Nat -> Nat -> Set where
   Base : forall {n} -> Leq n n
   Step : forall {n m} -> Leq n m -> Leq n (Succ m)

Now when you pattern match on the Base constructor you learn that the  
two numbers are equal. To achieve the same without using data, you  
need to pass around the equality proofs explicitly - which can be a  
bit less pleasant to work with. Best,

   Wouter

PS - In a somewhat related point, I recently spoke to Adam Chlipala  
who's been teaching a course using Coq. He wanted to expose his  
students some Agda as well, but found it hard to find convincing  
examples highlighting the differences between the two. Is anyone  
familiar enough with both systems to give an equitable comparison,  
either on the mailing list or wiki?


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.