[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.
A.
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