arith_3.vh (111B)
1 2 3 4 5 6 7 8
f : Int -> Int f n = n - 20 b : Nat b = 12 a = 2 + f b * 4 / 6 -- `b` will get automatically cast to an int.