[Agda] Agda Observational equality using primUnsafeTrustMe?

[Dan Doel]

On Friday 07 January 2011 7:04:49 pm Conor McBride wrote:
> On 7 Jan 2011, at 17:05, Thorsten Altenkirch wrote:
> > Hi Dominique,
> > 
> > I have been thinking about something like this but didn't realize it
> > could be done so easily. I think this is an interesting idea.
> > 
> > It certainly breaks a number of things, e.g. subject reduction. But
> > does it break termination?
> 
> Since it now is tomorrow, I can confirm that, yes, it does
> break termination.

To elaborate slightly on Conor's answer, the question is roughly the same as 
asking, "is it safe to erase/be lazy in equality proofs?" And the answer to 
that, for open terms, is "no."

-- Dan