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
Lean uses something close to this! github.com/leanprover/lea
1
Doesn't it get a bit clunky using a type-parametric equality in this definition?
1
Replying to
No clue. Might have to ask about that! I've not played with it too heavily to know what the trade-offs are.
We really only use one propositional equality in Lean, so I don't really know what alternatives would feel like either. As shown in the file, most equality proofs are squashed by `simp`. The code looks pretty reasonable to me.
1
My instinct is to define a custom equality on ℕ, perhaps:
_≈_ : ℕ → ℕ → Set
zero ≈ zero = ⊤
suc m ≈ suc n = m ≈ n
_ ≈ _ = ⊥
or an inductive type family doing something similar. It just cuts down on use of `cong suc`, `suc-injective`, and rewriting.
1
Show replies