[Agda] Abstract, definitional equality and propositional equality

[Andrés Sicard-Ramírez]

2011/8/9 Nils Anders Danielsson <nad at chalmers.se>:
> On 2011-08-09 17:26, Andrés Sicard-Ramírez wrote:
>>
>> Of course. In my current development, the abstract block is inside a
>> mutual
>> block, for example
>>
>> postulate
>>   foo bar : ℕ → ℕ
>>
>> mutual
>>   abstract
>>     a : ℕ
>>     a = foo b
>>
>>     b : ℕ
>>     b = bar a
>>
>>     thm₁ : a ≡ foo b
>>     thm₁ = {!refl!} -- Agda hangs
>>
>> thm₂ : a ≡ foo b
>> thm₂ = {!refl!}  -- Doesn't type check
>>
>> therefore I cannot prove a ≡ foo b inside the abstract block because Agda
>> hangs, so I need to prove the theorem outside the abstract block.
>
> I don't understand why you would want to do what you're doing, but can't
> you replace the abstract block with more postulates?

Due to your (implicit) negative answer, I rewrote what I need to prove
successful.
Thanks for your answer.

-- 
Andrés