val nth (#a: _) (n: nat) (#m: nat{m > n}) (v: vector a m) : a
val nth (#a: _) (n: nat) (#m: nat{m > n}) (v: vector a m) : a
let rec nth #a (n:nat) (#m:nat{m > n}) (v:vector a m) : a =
  let VCons x xs = v in // F* can prove that since m > n, m > 0, and so v <> VNil
  if n = 0
  then x
  else nth (n-1) xs
module OPLSS2021.Demo1

////////////////////////////////////////////////////////////////////////////////
// Vectors
////////////////////////////////////////////////////////////////////////////////

type vector (a:Type) : nat -> Type =
  | VNil : vector a 0
  | VCons : hd:a
          -> #n:nat //implicit argument, you don't have to write it in applications or patterns
          -> tl:vector a n
          -> vector a (n + 1)

let head' (v:vector 'a 'n { (match v with VCons _ _ -> true | _ -> false) }) : 'a =
  match v with
  | VCons x xs -> x

//VCons? v is syntactic sugar for saying that v is in the VCons case
let head (v:vector 'a 'n { VCons? v }) : 'a =
  match v with
  | VCons x xs -> x
/
prims.fst.checked FStar.Pervasives.fsti.checked
OPLSS2021.Demo1.fst
n: Prims.nat -> v: OPLSS2021.Demo1.vector a m -> a
Prims.nat Prims.b2t Prims.op_GreaterThan OPLSS2021.Demo1.vector Prims.op_Equality Prims.int Prims.bool OPLSS2021.Demo1.nth Prims.op_Subtraction
let rec nth #a (n: nat) (#m: nat{m > n}) (v: vector a m) : a =
  
let VCons x xs = v in
if n = 0 then x else nth (n - 1) xs