[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 16:34, Andrés Sicard-Ramírez wrote:
>>
>> abstract
>>   one : ℕ
>>   one = suc 0
>>
>>   thm₁ : one ≡ suc 0
>>   thm₁ = refl
>>
>> thm₂ : one ≡ suc 0
>> thm₂ = {!refl!}  -- Doesn't type check
>>
>> I am stuck in prove that one ≡ suc 0 outside the abstract block. Is it
>> possible?
>
> Yes, using thm₁.
>

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.

-- 
Andrés