src/gen_lib/vector.lem


1
2
3
4
5
6
7
8
9

open import Pervasives

type bit = O | I | U
type vector 'a = V of list 'a * nat * bool

let rec nth xs (n : nat) = match (n,xs) with
  | (0,x :: xs) -> x
  | (n + 1,x :: xs) -> nth xs n
end