[Agda] Abstract, definitional equality and propositional equality

[Nils Anders Danielsson]

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?

-- 
/NAD