data Vec A : ℕ → Set where
[] : Vec A zero
_∷_ : A → Vec A n → Vec A (suc n)
--vs--
record Vec A n : Set where
constructor tabulate
field
lookup : Fin n → A
--vs--
Vec : Set → ℕ → Set
Vec A zero = ⊤
Vec A (suc n) = A × Vec A n
Fight!
Conversation
There's also
Vec A n = Σ[ xs ∈ List A ] length xs ≈ n
where _≈_ is nicely computing equality for ℕ.
2
3
Replying to
Doesn't it get a bit clunky using a type-parametric equality in this definition?
1
No clue. Might have to ask about that! I've not played with it too heavily to know what the trade-offs are.
1
Show replies