[Agda] Abstract, definitional equality and propositional equality

[Nils Anders Danielsson]

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₁.

-- 
/NAD