[Agda] Irrelevance and propositional equality

[Alan Jeffrey]

My foot thanks you.

A.

On 07/29/2011 02:11 PM, Andreas Abel wrote:
> Hi Alan,
>
> Well, for one, any use of trustMe does not destroy the termination
> property, so you should not be able to write programs that make the type
> checker loop (at least the ideal bug-free implementation of Agda ;-)).
>
> Also, your use of trustMe does not endanger consistency, because any
> closed proof of a == b is refl, hence, requiring a to be identical to b.
>    It does not matter that your proof is irrelevant here.  So, there is
> still no closed proof of 1 == 0 possible with your use of trustMe.
>
> So, I think your foot is safe. ;-)
>
> Actually, this looks like a nice combination of experimental features...
>
> Cheers,
> Andreas
>
>
> On 7/20/11 4:23 PM, Alan Jeffrey wrote:
>> I'm currently working on some code where life is remarkably easier if I
>> make use of a function which promotes irrelevant propositional
>> equalities to relevant ones:
>>
>> ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)
>> ≡-relevant a≡b = trustMe
>>
>> Of course, life would also be remarkably easier if I were to postulate
>> false. Am I shooting myself in the foot here?
>>
>> A.
>>
>