Fin, Vect and restrict in idris

prepend_to_group : {tsm1 : Nat} -> (rsize : Nat) -> Nat -> Vect rsize x -> Vect (S tsm1) x -> Vect (S rsize) x
interface ContainsBytes a where
get_byte : a -> Nat -> Nat
implementation ContainsBytes (Vect (S l) Nat) where
get_byte a n = ?get_byte_of_vect_impl
Can’t solve constraint between: pred (length a) and l
vectLengthIsL : {ll : Nat} -> (v : Vect ll x) -> length v = ll
vectLengthIsL Vect.Nil = Refl
vectLengthIsL (Vect.(::) _ rest) =
rewrite vectLengthIsL rest in
Refl
ifVectLenIsSLThenPredVectLenIsL : {ll : Nat} -> (v : Vect (S ll) x) -> pred (length v) = ll
ifVectLenIsSLThenPredVectLenIsL v =
rewrite vectLengthIsL v in
Refl
implementation ContainsBytes (Vect (S l) Nat) where
get_byte a n =
let
lastElementOf : Nat
lastElementOf = pred (length a)
indexIntoVect : Fin (S l)
indexIntoVect =
rewrite sym (ifVectLenIsSLThenPredVectLenIsL a) in
restrict lastElementOf (cast n) -- Fin (S (pred (length a)))
in
index indexIntoVect a

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
art yerkes

art yerkes

An old programmer learning new tricks.