[Agda] Agda Observational equality using primUnsafeTrustMe?

[Dominique Devriese]

Conor, Dan, Thorsten,

Thanks for the interesting responses, I think I better understand the
problem now.

Dominique

2011/1/9 Conor McBride <conor at strictlypositive.org>:
>
> On 9 Jan 2011, at 14:44, Thorsten Altenkirch wrote:
>
>> Ok, even if we only postulate ext : ((x: A) -> f x = g s) -> f = g and add
>> an equality ext p = refl then p may be a lie but subst (ext p) reduces which
>> can cause non-termination.
>
> By the way, it is possible to construct a counterexample in the
> manner you suggest, but in which p is not a lie.
>
> Cheers
>
> Conor
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>