[Agda] Abstract, definitional equality and propositional equality

[Andrés Sicard-Ramírez]

Hi,

Given

open import Data.Nat
open import Relation.Binary.PropositionalEquality

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?

Thanks,

-- 
Andrés