[Agda] Re: Builtins

Nils Anders Danielsson nad at cse.gu.se
Tue Apr 28 18:27:12 CEST 2015


On 2015-04-25 20:53, Kirill Elagin wrote:
> Also note, that in Agda’s stdlib from `a ≡ b` it follows that `a` is
> `b`, [...]

This is not true in general for open terms.

-- 
/NAD



More information about the Agda mailing list