[Agda] reflective access to definitional equality

Wouter Swierstra wss at cs.nott.ac.uk
Wed Mar 10 21:18:27 CET 2010


> So, I thought, what if I could write contains in such a way that the
> above reduced to True *definitionally*?  
> 
> pf x y z = Refl

I believe Ulf implemented something a bit similar at the last Agda Implementors' Meeting. There's a primitive function:

  trustMe : {A : Set}{a b : A} -> a ≡ b

that is guaranteed to reduce to Refl on definitionally equal inputs. There's some sparse documentation in the release notes:

  http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-2-6

Hope this helps,

  Wouter



More information about the Agda mailing list