[Agda] Re: Do we really want special case casts?

[Nils Anders Danielsson]

On 2009-10-17 20:19, Samuel Gélineau wrote:
> But whenever we wish to write a proof involving the fact that some
> name is a type constant, we must write a special case proof.

You can also parametrise the general proof on a proof of injectivity.
See the following old discussion on this subject:

  http://thread.gmane.org/gmane.comp.lang.agda/954

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