[Agda] Trust me regarding Dan Licata's trick

Alan Jeffrey ajeffrey at bell-labs.com
Thu Jun 6 22:57:20 CEST 2013

In the JS back end, _==_ is recognized as a singleton type, so any 
expressions of this type are eta-converted at compile time to refl, 
including uses of primTrustMe.


On 06/06/2013 03:09 PM, Nils Anders Danielsson wrote:
> On 2013-06-06 13:36, Martin Escardo wrote:
>> But it would be nice to hear from those who designed and implemented
>> the feature.
> I don't have much to add to this discussion. (Ulf implemented
> primTrustMe, I added some kind of support to MAlonzo.)

More information about the Agda mailing list