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

--

--

--

An old programmer learning new tricks.

Love podcasts or audiobooks? Learn on the go with our new app.

Recommended from Medium

Pros and Cons of BP Logix - with a BP Logix Alternative

CS373 Spring 2022: Joriann Bassi

Download Quran For Android 4.0

Git hooks to the rescue !!!

Microsoft Power Platform: Setup a Trial Environment

Microsoft Power Platform Trial Environment

1st Academic Paper by Apache ShardingSphere Accepted by ICDE, A Top-Level Database Conference

How to find out who has Shoretel Video Calls licences applied to their account

A Reporting Tool

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.

More from Medium

Exchange messages with IBM MQ using Rust

Scalable live streaming (using WebRTC)

An overview of version control and non-relational databases

RabbitMQ: Smart Decoupling Rabbits!