[Agda] heterogeneous equality

[Nils Anders Danielsson]

On 2010-09-09 13:53, Andrés Sicard-Ramírez wrote:
> Does it mean that using the option --injective-type-constructors your
> example should type check?

No.  Is anyone using --injective-type-constructors?

-- 
/NAD