(* * This example shows that no array bounds checking * is needed for dot product. *) (* 2 type annotations, which occupy 2 lines *) assert length <| {n:nat} int array(n) -> int(n) and sub <| {n:nat, i:nat | i < n } int array(n) * int(i) -> int fun{p:nat} dotprod(v1, v2) = let fun loop(i, n, sum) = if i = n then sum else loop(i+1, n, sum + sub(v1, i) * sub(v2, i)) where loop <| {i:nat | i <= p} int(i) * int(p) * int -> int in loop(0, length v1, 0) end where dotprod <| {q:nat | p <= q } int array(p) * int array(q) -> int