2
module InferrableFields where
8
data Vec A : ℕ → Set where
10
_∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)
12
record SomeVec A : Set where
16
open SomeVec using (unpack)
18
pack : ∀ {A n} → Vec A n -> SomeVec A
19
pack xs = record { unpack = xs }
21
data _≡_ {A : Set}(x : A) : A → Set where
24
lemPack : ∀ {A}(xs : SomeVec A) → pack (unpack xs) ≡ xs
b'\\ No newline at end of file'