[Agda] Trust me regarding Dan Licata's trick

Nils Anders Danielsson nad at cse.gu.se
Thu Jun 6 23:33:36 CEST 2013

On 2013-06-06 22:57, Alan Jeffrey wrote:
> 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.

The Epic backend contains similar functionality. From the release notes
for 2.3.0:

   "An important example of an inferable type is the usual propositional
   equality type (_≡_). Any function returning a propositional equality
   can simply return the reflexivity constructor directly without
   computing anything."


More information about the Agda mailing list