[Agda] INLINE-pragma

Nils Anders Danielsson nad at cse.gu.se
Tue Mar 6 11:14:05 CET 2018


On 2018-03-02 16:26, Frederik Hanghøj Iversen wrote:
> Is it possible to normalize something to the first visible
> constructors?

I don't think there's any support for that at the moment. Perhaps you
could try to implement it yourself.

-- 
/NAD


More information about the Agda mailing list