Smart Case [Re: [Agda] A puzzle with "with"]

[Nils Anders Danielsson]

On 2009-07-03 20:09, Thorsten Altenkirch wrote:
>> Consider the booleans with identity and negation defined by case
>> distinction. Then, the constraints
>>
>> id  x = true
>> not x = true
> 
> I don't understand this, since "id x" is not normal, but if we reduce it 
> it becomes x=true and hence not x reduces to false and this is 
> inconsistent.

I think you should read Andreas' statement as "(identity and negation)
defined by case distinction", not "identity and (negation defined by
case distinction)".

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