F* code from Munich Lambda meetup, 2017-05-17

lambda.fst

module Lambda

open FStar.Mul

val factorial: n:nat -> Tot (y:nat{y >= 1 /\ y >= n})
let rec factorial n =
  if n = 0 then
    1
  else
    n * factorial (n - 1)

type vector 'a : nat -> Type =
  | VNil: vector 'a 0
  | VCons: hd:'a -> #n:nat -> tl:vector 'a n -> vector 'a (n + 1)

val vec_of_three_nats: vector nat 3
let vec_of_three_nats = VCons 0 (VCons 1 (VCons 2 VNil))

type pos = n:nat{n > 0}

val head: #a:Type -> #n:pos -> vector a n -> Tot a
let head #a #n v =
  match v with
    | VCons x xs -> x

val nth : n:nat -> #m:nat{m > n} -> vector 'a m -> Tot 'a
let rec nth n #m (VCons x #m' xs) =
  if n = 0 then
    x
  else
    nth (n-1) #m' xs

val map_vec: ('a -> Tot 'b) -> #n:nat -> vector 'a n -> Tot (vector 'b n)
let rec map_vec f #n v =
  match v with
    | VNil -> VNil
    | VCons hd tl -> VCons (f hd) (map_vec f tl)

val append: #n:nat -> #m:nat -> vector 'a n -> vector 'a m ->  Tot (vector 'a (n + m))
let rec append #a #n #m v1 v2 =
  match v1 with
    | VNil -> v2
    | VCons hd tl -> VCons hd (append tl v2)

val reverse: #n:nat -> vector 'a n -> Tot (vector 'a n)
let rec reverse #a #n v =
  match v with
    | VNil -> VNil
    | VCons hd tl -> append (reverse tl) (VCons hd VNil)

val snoc: #n:nat -> vector 'a n -> 'a -> Tot (vector 'a (n + 1))
let snoc #a #n v x = append v (VCons x VNil)

val snoc_cons: #a:eqtype -> #n:nat -> v:vector a n -> x:a -> Lemma (reverse (snoc v x) = VCons x (reverse v))
let rec snoc_cons #a #n v x =
  match v with
    | VNil -> ()
    | VCons hd tl -> snoc_cons tl x


val rev_rev: #a:eqtype -> #n:nat -> v:vector a n -> Lemma (reverse (reverse v) = v)
let rec rev_rev #a #n v =
  match v with
    | VNil -> ()
    | VCons hd tl -> rev_rev tl; snoc_cons (reverse tl) hd