1
2
3
4
5
6
7
8
9
10
11
type ``{0} ∪ ℕ<0xFFFFFFFF`` = uint32
type ``ℤ∗<0xFFFFFFFF``      = uint32

let ``42`` : ``{0} ∪ ℕ<0xFFFFFFFF`` = 42u

let add : ``ℤ∗<0xFFFFFFFF`` -> ``ℤ∗<0xFFFFFFFF`` -> ``ℤ∗<0xFFFFFFFF`` =
  fun x y ->
    x + y

let result1 = ``42``
let result2 = add 42u 42u

> type {0} ∪ ℕ<0xFFFFFFFF = uint32
> type ℤ∗<0xFFFFFFFF = uint32
> val 42 : {0} ∪ ℕ<0xFFFFFFFF = 42u
> val add : x:ℤ∗<0xFFFFFFFF -> y:ℤ∗<0xFFFFFFFF -> ℤ∗<0xFFFFFFFF
> val result1 : {0} ∪ ℕ<0xFFFFFFFF = 42u
> val result2 : ℤ∗<0xFFFFFFFF = 84u