[Agda] I want implicit coercions in Agda

Nils Anders Danielsson nad at cse.gu.se
Fri Nov 23 11:21:12 CET 2018


On 23/11/2018 10.34, Nicolas Pouillard wrote:
> To me a concrete first step would build around a Coerce record and
> instance arguments plus some syntactic help to use it. Would it make
> sense to reuse idiom brackets?

Why do you need new syntax for this?

-- 
/NAD


More information about the Agda mailing list