JS.Union

Union types (= sum types) in the FFI.

Definitions

data NPP : (Type -> Type -> Type) -> List Type -> List Type -> Type

Totality: total
Visibility: public export
Constructors:

Nil : NPP f [] []

(::) : f a b -> NPP f ps1 ps2 -> NPP f (a :: ps1) (b :: ps2)

Hints:

NPP FromFFI [a, b] [m, n] => All SafeCast [m, n] => FromFFI (HSum [a, b]) (Union2 m n)

NPP FromFFI [a, b, c] [m, n, o] => All SafeCast [m, n, o] => FromFFI (HSum [a, b, c]) (Union3 m n o)

NPP FromFFI [a, b, c, d] [m, n, o, p] => All SafeCast [m, n, o, p] => FromFFI (HSum [a, b, c, d]) (Union4 m n o p)

NPP FromFFI [a, b, c, d, e] [m, n, o, p, r] => All SafeCast [m, n, o, p, r] => FromFFI (HSum [a, b, c, d, e]) (Union5 m n o p r)

NPP FromFFI [a, b, c, d, e, f] [m, n, o, p, r, s] => All SafeCast [m, n, o, p, r, s] => FromFFI (HSum [a, b, c, d, e, f]) (Union6 m n o p r s)

NPP FromFFI [a, b, c, d, e, f, g] [m, n, o, p, r, s, t] => All SafeCast [m, n, o, p, r, s, t] => FromFFI (HSum [a, b, c, d, e, f, g]) (Union7 m n o p r s t)

NPP FromFFI [a, b, c, d, e, f, g, h] [m, n, o, p, r, s, t, u] => All SafeCast [m, n, o, p, r, s, t, u] => FromFFI (HSum [a, b, c, d, e, f, g, h]) (Union8 m n o p r s t u)

NPP FromFFI [a, b, c, d, e, f, g, h, i] [m, n, o, p, r, s, t, u, v] => All SafeCast [m, n, o, p, r, s, t, u, v] => FromFFI (HSum [a, b, c, d, e, f, g, h, i]) (Union9 m n o p r s t u v)

NPP FromFFI [a, b, c, d, e, f, g, h, i, j] [m, n, o, p, r, s, t, u, v, w] => All SafeCast [m, n, o, p, r, s, t, u, v, w] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j]) (Union10 m n o p r s t u v w)

NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k] [m, n, o, p, q, r, s, t, u, v, w] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k]) (Union11 m n o p q r s t u v w)

NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k, l] [m, n, o, p, q, r, s, t, u, v, w, x] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w, x] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l]) (Union12 m n o p q r s t u v w x)

NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1] [m, n, o, p, q, r, s, t, u, v, w, x, y] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w, x, y] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1]) (Union13 m n o p q r s t u v w x y)

NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2] [m, n, o, p, q, r, s, t, u, v, w, x, y, z] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w, x, y, z] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2]) (Union14 m n o p q r s t u v w x y z)

NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3] [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3]) (Union15 m n o p q r s t u v w x y z z1)

NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3, a4] [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1, z2] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1, z2] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3, a4]) (Union16 m n o p q r s t u v w x y z z1 z2)

NPP ToFFI [a, b] [m, n] => ToFFI (HSum [a, b]) (Union2 m n)

NPP ToFFI [a, b, c] [m, n, o] => ToFFI (HSum [a, b, c]) (Union3 m n o)

NPP ToFFI [a, b, c, d] [m, n, o, p] => ToFFI (HSum [a, b, c, d]) (Union4 m n o p)

NPP ToFFI [a, b, c, d, e] [m, n, o, p, q] => ToFFI (HSum [a, b, c, d, e]) (Union5 m n o p q)

NPP ToFFI [a, b, c, d, e, f] [m, n, o, p, q, r] => ToFFI (HSum [a, b, c, d, e, f]) (Union6 m n o p q r)

NPP ToFFI [a, b, c, d, e, f, g] [m, n, o, p, q, r, s] => ToFFI (HSum [a, b, c, d, e, f, g]) (Union7 m n o p q r s)

NPP ToFFI [a, b, c, d, e, f, g, h] [m, n, o, p, q, r, s, t] => ToFFI (HSum [a, b, c, d, e, f, g, h]) (Union8 m n o p q r s t)

NPP ToFFI [a, b, c, d, e, f, g, h, i] [m, n, o, p, q, r, s, t, u] => ToFFI (HSum [a, b, c, d, e, f, g, h, i]) (Union9 m n o p q r s t u)

NPP ToFFI [a, b, c, d, e, f, g, h, i, j] [m, n, o, p, q, r, s, t, u, v] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j]) (Union10 m n o p q r s t u v)

NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k] [m, n, o, p, q, r, s, t, u, v, w] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k]) (Union11 m n o p q r s t u v w)

NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k, l] [m, n, o, p, q, r, s, t, u, v, w, x] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l]) (Union12 m n o p q r s t u v w x)

NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1] [m, n, o, p, q, r, s, t, u, v, w, x, y] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1]) (Union13 m n o p q r s t u v w x y)

NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2] [m, n, o, p, q, r, s, t, u, v, w, x, y, z] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2]) (Union14 m n o p q r s t u v w x y z)

NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3] [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3]) (Union15 m n o p q r s t u v w x y z z1)

NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3, a4] [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1, z2] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3, a4]) (Union16 m n o p q r s t u v w x y z z1 z2)

data Union2 : Type -> Type -> Type

Totality: total
Visibility: export
Hints:

NPP FromFFI [a, b] [m, n] => All SafeCast [m, n] => FromFFI (HSum [a, b]) (Union2 m n)

FromFFI (Union2 a b) (Union2 a b)

NPP ToFFI [a, b] [m, n] => ToFFI (HSum [a, b]) (Union2 m n)

ToFFI (Union2 a b) (Union2 a b)

toUnion2 : HSum [a, b] -> Union2 a b

Totality: total
Visibility: export

fromUnion2 : All SafeCast [a, b] => Union2 a b -> Maybe (HSum [a, b])

Totality: total
Visibility: export

data Union3 : Type -> Type -> Type -> Type

Totality: total
Visibility: export
Hints:

NPP FromFFI [a, b, c] [m, n, o] => All SafeCast [m, n, o] => FromFFI (HSum [a, b, c]) (Union3 m n o)

FromFFI (Union3 a b c) (Union3 a b c)

NPP ToFFI [a, b, c] [m, n, o] => ToFFI (HSum [a, b, c]) (Union3 m n o)

ToFFI (Union3 a b c) (Union3 a b c)

toUnion3 : HSum [a, b, c] -> Union3 a b c

Totality: total
Visibility: export

fromUnion3 : All SafeCast [a, b, c] => Union3 a b c -> Maybe (HSum [a, b, c])

Totality: total
Visibility: export

data Union4 : Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: export
Hints:

NPP FromFFI [a, b, c, d] [m, n, o, p] => All SafeCast [m, n, o, p] => FromFFI (HSum [a, b, c, d]) (Union4 m n o p)

FromFFI (Union4 a b c d) (Union4 a b c d)

NPP ToFFI [a, b, c, d] [m, n, o, p] => ToFFI (HSum [a, b, c, d]) (Union4 m n o p)

ToFFI (Union4 a b c d) (Union4 a b c d)

toUnion4 : HSum [a, b, c, d] -> Union4 a b c d

Totality: total
Visibility: export

fromUnion4 : All SafeCast [a, b, c, d] => Union4 a b c d -> Maybe (HSum [a, b, c, d])

Totality: total
Visibility: export

data Union5 : Type -> Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: export
Hints:

NPP FromFFI [a, b, c, d, e] [m, n, o, p, r] => All SafeCast [m, n, o, p, r] => FromFFI (HSum [a, b, c, d, e]) (Union5 m n o p r)

FromFFI (Union5 a b c d e) (Union5 a b c d e)

NPP ToFFI [a, b, c, d, e] [m, n, o, p, q] => ToFFI (HSum [a, b, c, d, e]) (Union5 m n o p q)

ToFFI (Union5 a b c d e) (Union5 a b c d e)

toUnion5 : HSum [a, b, c, d, e] -> Union5 a b c d e

Totality: total
Visibility: export

fromUnion5 : All SafeCast [a, b, c, d, e] => Union5 a b c d e -> Maybe (HSum [a, b, c, d, e])

Totality: total
Visibility: export

data Union6 : Type -> Type -> Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: export
Hints:

NPP FromFFI [a, b, c, d, e, f] [m, n, o, p, r, s] => All SafeCast [m, n, o, p, r, s] => FromFFI (HSum [a, b, c, d, e, f]) (Union6 m n o p r s)

FromFFI (Union6 a b c d e f) (Union6 a b c d e f)

NPP ToFFI [a, b, c, d, e, f] [m, n, o, p, q, r] => ToFFI (HSum [a, b, c, d, e, f]) (Union6 m n o p q r)

ToFFI (Union6 a b c d e f) (Union6 a b c d e f)

toUnion6 : HSum [a, b, c, d, e, f] -> Union6 a b c d e f

Totality: total
Visibility: export

fromUnion6 : All SafeCast [a, b, c, d, e, f] => Union6 a b c d e f -> Maybe (HSum [a, b, c, d, e, f])

Totality: total
Visibility: export

data Union7 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: export
Hints:

NPP FromFFI [a, b, c, d, e, f, g] [m, n, o, p, r, s, t] => All SafeCast [m, n, o, p, r, s, t] => FromFFI (HSum [a, b, c, d, e, f, g]) (Union7 m n o p r s t)

FromFFI (Union7 a b c d e f g) (Union7 a b c d e f g)

NPP ToFFI [a, b, c, d, e, f, g] [m, n, o, p, q, r, s] => ToFFI (HSum [a, b, c, d, e, f, g]) (Union7 m n o p q r s)

ToFFI (Union7 a b c d e f g) (Union7 a b c d e f g)

toUnion7 : HSum [a, b, c, d, e, f, g] -> Union7 a b c d e f g

Totality: total
Visibility: export

fromUnion7 : All SafeCast [a, b, c, d, e, f, g] => Union7 a b c d e f g -> Maybe (HSum [a, b, c, d, e, f, g])

Totality: total
Visibility: export

data Union8 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: export
Hints:

NPP FromFFI [a, b, c, d, e, f, g, h] [m, n, o, p, r, s, t, u] => All SafeCast [m, n, o, p, r, s, t, u] => FromFFI (HSum [a, b, c, d, e, f, g, h]) (Union8 m n o p r s t u)

FromFFI (Union8 a b c d e f g h) (Union8 a b c d e f g h)

NPP ToFFI [a, b, c, d, e, f, g, h] [m, n, o, p, q, r, s, t] => ToFFI (HSum [a, b, c, d, e, f, g, h]) (Union8 m n o p q r s t)

ToFFI (Union8 a b c d e f g h) (Union8 a b c d e f g h)

toUnion8 : HSum [a, b, c, d, e, f, g, h] -> Union8 a b c d e f g h

Totality: total
Visibility: export

fromUnion8 : All SafeCast [a, b, c, d, e, f, g, h] => Union8 a b c d e f g h -> Maybe (HSum [a, b, c, d, e, f, g, h])

Totality: total
Visibility: export

data Union9 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: export
Hints:

NPP FromFFI [a, b, c, d, e, f, g, h, i] [m, n, o, p, r, s, t, u, v] => All SafeCast [m, n, o, p, r, s, t, u, v] => FromFFI (HSum [a, b, c, d, e, f, g, h, i]) (Union9 m n o p r s t u v)

FromFFI (Union9 a b c d e f g h i) (Union9 a b c d e f g h i)

NPP ToFFI [a, b, c, d, e, f, g, h, i] [m, n, o, p, q, r, s, t, u] => ToFFI (HSum [a, b, c, d, e, f, g, h, i]) (Union9 m n o p q r s t u)

ToFFI (Union9 a b c d e f g h i) (Union9 a b c d e f g h i)

toUnion9 : HSum [a, b, c, d, e, f, g, h, i] -> Union9 a b c d e f g h i

Totality: total
Visibility: export

fromUnion9 : All SafeCast [a, b, c, d, e, f, g, h, i] => Union9 a b c d e f g h i -> Maybe (HSum [a, b, c, d, e, f, g, h, i])

Totality: total
Visibility: export

data Union10 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: export
Hints:

NPP FromFFI [a, b, c, d, e, f, g, h, i, j] [m, n, o, p, r, s, t, u, v, w] => All SafeCast [m, n, o, p, r, s, t, u, v, w] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j]) (Union10 m n o p r s t u v w)

FromFFI (Union10 a b c d e f g h i j) (Union10 a b c d e f g h i j)

NPP ToFFI [a, b, c, d, e, f, g, h, i, j] [m, n, o, p, q, r, s, t, u, v] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j]) (Union10 m n o p q r s t u v)

ToFFI (Union10 a b c d e f g h i j) (Union10 a b c d e f g h i j)

toUnion10 : HSum [a, b, c, d, e, f, g, h, i, j] -> Union10 a b c d e f g h i j

Totality: total
Visibility: export

fromUnion10 : All SafeCast [a, b, c, d, e, f, g, h, i, j] => Union10 a b c d e f g h i j -> Maybe (HSum [a, b, c, d, e, f, g, h, i, j])

Totality: total
Visibility: export

data Union11 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: export
Hints:

NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k] [m, n, o, p, q, r, s, t, u, v, w] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k]) (Union11 m n o p q r s t u v w)

FromFFI (Union11 a b c d e f g h i j k) (Union11 a b c d e f g h i j k)

NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k] [m, n, o, p, q, r, s, t, u, v, w] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k]) (Union11 m n o p q r s t u v w)

ToFFI (Union11 a b c d e f g h i j k) (Union11 a b c d e f g h i j k)

toUnion11 : HSum [a, b, c, d, e, f, g, h, i, j, k] -> Union11 a b c d e f g h i j k

Totality: total
Visibility: export

fromUnion11 : All SafeCast [a, b, c, d, e, f, g, h, i, j, k] => Union11 a b c d e f g h i j k -> Maybe (HSum [a, b, c, d, e, f, g, h, i, j, k])

Totality: total
Visibility: export

data Union12 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: export
Hints:

NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k, l] [m, n, o, p, q, r, s, t, u, v, w, x] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w, x] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l]) (Union12 m n o p q r s t u v w x)

FromFFI (Union12 a b c d e f g h i j k l) (Union12 a b c d e f g h i j k l)

NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k, l] [m, n, o, p, q, r, s, t, u, v, w, x] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l]) (Union12 m n o p q r s t u v w x)

ToFFI (Union12 a b c d e f g h i j k l) (Union12 a b c d e f g h i j k l)

toUnion12 : HSum [a, b, c, d, e, f, g, h, i, j, k, l] -> Union12 a b c d e f g h i j k l

Totality: total
Visibility: export

fromUnion12 : All SafeCast [a, b, c, d, e, f, g, h, i, j, k, l] => Union12 a b c d e f g h i j k l -> Maybe (HSum [a, b, c, d, e, f, g, h, i, j, k, l])

Totality: total
Visibility: export

data Union13 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: export
Hints:

NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1] [m, n, o, p, q, r, s, t, u, v, w, x, y] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w, x, y] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1]) (Union13 m n o p q r s t u v w x y)

FromFFI (Union13 a b c d e f g h i j k l m) (Union13 a b c d e f g h i j k l m)

NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1] [m, n, o, p, q, r, s, t, u, v, w, x, y] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1]) (Union13 m n o p q r s t u v w x y)

ToFFI (Union13 a b c d e f g h i j k l m) (Union13 a b c d e f g h i j k l m)

toUnion13 : HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1] -> Union13 a b c d e f g h i j k l a1

Totality: total
Visibility: export

fromUnion13 : All SafeCast [a, b, c, d, e, f, g, h, i, j, k, l, a1] => Union13 a b c d e f g h i j k l a1 -> Maybe (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1])

Totality: total
Visibility: export

data Union14 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: export
Hints:

NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2] [m, n, o, p, q, r, s, t, u, v, w, x, y, z] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w, x, y, z] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2]) (Union14 m n o p q r s t u v w x y z)

FromFFI (Union14 a b c d e f g h i j k l m n) (Union14 a b c d e f g h i j k l m n)

NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2] [m, n, o, p, q, r, s, t, u, v, w, x, y, z] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2]) (Union14 m n o p q r s t u v w x y z)

ToFFI (Union14 a b c d e f g h i j k l m n) (Union14 a b c d e f g h i j k l m n)

toUnion14 : HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2] -> Union14 a b c d e f g h i j k l a1 a2

Totality: total
Visibility: export

fromUnion14 : All SafeCast [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2] => Union14 a b c d e f g h i j k l a1 a2 -> Maybe (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2])

Totality: total
Visibility: export

data Union15 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: export
Hints:

NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3] [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3]) (Union15 m n o p q r s t u v w x y z z1)

FromFFI (Union15 a b c d e f g h i j k l m n o) (Union15 a b c d e f g h i j k l m n o)

NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3] [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3]) (Union15 m n o p q r s t u v w x y z z1)

ToFFI (Union15 a b c d e f g h i j k l m n o) (Union15 a b c d e f g h i j k l m n o)

toUnion15 : HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3] -> Union15 a b c d e f g h i j k l a1 a2 a3

Totality: total
Visibility: export

fromUnion15 : All SafeCast [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3] => Union15 a b c d e f g h i j k l a1 a2 a3 -> Maybe (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3])

Totality: total
Visibility: export

data Union16 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: export
Hints:

NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3, a4] [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1, z2] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1, z2] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3, a4]) (Union16 m n o p q r s t u v w x y z z1 z2)

FromFFI (Union16 a b c d e f g h i j k l m n o p) (Union16 a b c d e f g h i j k l m n o p)

NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3, a4] [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1, z2] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3, a4]) (Union16 m n o p q r s t u v w x y z z1 z2)

ToFFI (Union16 a b c d e f g h i j k l m n o p) (Union16 a b c d e f g h i j k l m n o p)

toUnion16 : HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3, a4] -> Union16 a b c d e f g h i j k l a1 a2 a3 a4

Totality: total
Visibility: export

fromUnion16 : All SafeCast [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3, a4] => Union16 a b c d e f g h i j k l a1 a2 a3 a4 -> Maybe (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3, a4])

Totality: total
Visibility: export