1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
module FstarList (* Don't use Fstar as module name *)

(* If used in type refinements, you must specify return effects, Ex: "Tot".
  But always use the most precise type as it possible *)
val length : xs:list 'a -> Tot (r:int{r >= 0})
let rec length xs = match xs with
  | [   ] -> 0
  | x::xs -> 1 + length xs

(* Only two branches in pattern matching are needed. _,[] and [],_
  are not neccesary *)
val zip : 
    xs:list 'a -> 
    ys:list 'b {length xs = length ys} -> 
    Tot (r:list ('a * 'b) {length r = length xs && length r = length ys})
let rec zip xs ys = match xs,ys with
  | [   ],[   ] -> []
  | x::xs,y::ys -> (x,y) :: zip xs ys

Verifying module: FStar.FunctionalExtensionality
Verifying module: FStar.Set 
Verifying module: FStar.Heap 
Verifying module: FStar.ST 
Verifying module: FStar.All 
Verifying module: Welcome 
All verification conditions discharged successfully

1
2
3
4
5
6
7
8
9
let rec zip xs ys = (xs,ys) |> function
  | [   ],[   ] -> []
  | _____,[   ] -> failwith "xs and ys aren't of same length"
  | [   ],_____ -> failwith "xs and ys aren't of same length"
  | x::xs,y::ys -> (x,y) :: zip xs ys

(* Note: | _____,[   ] | [   ],_____ -> failwith "..." isn't supported *)

let r = zip [1 .. 10] ['a' .. 'z']

> 
System.Exception: xs and ys aren't of same length
  at Microsoft.FSharp.Core.Operators.FailWith[T](String message)
  at FSI_0004.zip[a,b](FSharpList`1 xs, FSharpList`1 ys) in C:\tmp\zip.fsx:line 5
  at FSI_0004.zip[a,b](FSharpList`1 xs, FSharpList`1 ys) in C:\tmp\zip.fsx:line 5
  at FSI_0004.zip[a,b](FSharpList`1 xs, FSharpList`1 ys) in C:\tmp\zip.fsx:line 5
  at FSI_0004.zip[a,b](FSharpList`1 xs, FSharpList`1 ys) in C:\tmp\zip.fsx:line 5
  at FSI_0004.zip[a,b](FSharpList`1 xs, FSharpList`1 ys) in C:\tmp\zip.fsx:line 5
  at FSI_0004.zip[a,b](FSharpList`1 xs, FSharpList`1 ys) in C:\tmp\zip.fsx:line 5
  at FSI_0004.zip[a,b](FSharpList`1 xs, FSharpList`1 ys) in C:\tmp\zip.fsx:line 5
  at FSI_0004.zip[a,b](FSharpList`1 xs, FSharpList`1 ys) in C:\tmp\zip.fsx:line 5
  at FSI_0004.zip[a,b](FSharpList`1 xs, FSharpList`1 ys) in C:\tmp\zip.fsx:line 5
  at FSI_0004.zip[a,b](FSharpList`1 xs, FSharpList`1 ys) in C:\tmp\zip.fsx:line 5
  at <StartupCode$FSI_0005>.$FSI_0005.main@() in C:\tmp\zip.fsx:line 9
Stopped due to error