diff --git a/docs/conf.py b/docs/conf.py
--- a/docs/conf.py
+++ b/docs/conf.py
@@ -108,7 +108,7 @@
 
     tokens = {
         'root': [
-            (r'(if|then|else|let|loop|in|val|for|do|with|local|open|include|import|type|entry|module|while|module)\b', token.Keyword),
+            (r'(if|then|else|let|loop|in|val|for|do|with|local|open|include|import|type|def|entry|module|while|module)\b', token.Keyword),
             (r"#?[a-zA-Z_][a-zA-Z0-9_']*", token.Name),
             (r"--.*", token.Comment),
             (r'.', token.Text)
diff --git a/docs/language-reference.rst b/docs/language-reference.rst
--- a/docs/language-reference.rst
+++ b/docs/language-reference.rst
@@ -220,7 +220,7 @@
 names bound by preceding declarations.
 
 .. productionlist::
-   dec:   `fun_bind` | `val_bind` | `type_bind` | `mod_bind` | `mod_type_bind`
+   dec:   `val_bind` | `type_bind` | `mod_bind` | `mod_type_bind`
       : | "open" `mod_exp`
       : | "import" `stringlit`
       : | "local" `dec`
@@ -239,17 +239,16 @@
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. productionlist::
-   fun_bind:   ("let" | "entry") (`id` | "(" `binop` ")") `type_param`* `pat`+ [":" `type`] "=" `exp`
-           : | ("let" | "entry") `pat` `binop` `pat` [":" `type`] "=" `exp`
+   val_bind:   ("def" | "entry" | "let") (`id` | "(" `binop` ")") `type_param`* `pat`+ [":" `type`] "=" `exp`
+           : | ("def" | "entry" | "let") `pat` `binop` `pat` [":" `type`] "=" `exp`
 
-.. productionlist::
-   val_bind: "let" `id` [":" `type`] "=" `exp`
+**Note:** using ``let`` to define top-level bindings is deprecated.
 
-Functions and values must be defined before they are used.  A function
+Functions and constants must be defined before they are used.  A function
 declaration must specify the name, parameters, and body
 of the function::
 
-  let name params...: rettype = body
+  def name params...: rettype = body
 
 Hindley-Milner-style type inference is supported.  A parameter may be
 given a type with the notation ``(name: type)``.  Functions may not be
@@ -258,13 +257,13 @@
 by using type parameters, in the same way as for `Type
 Abbreviations`_::
 
-  let reverse [n] 't (xs: [n]t): [n]t = xs[::-1]
+  def reverse [n] 't (xs: [n]t): [n]t = xs[::-1]
 
 Type parameters for a function do not need to cover the types of all
 parameters.  The type checker will add more if necessary.  For
 example, the following is well typed::
 
-  let pair 'a (x: a) y = (x, y)
+  def pair 'a (x: a) y = (x, y)
 
 A new type variable will be invented for the parameter ``y``.
 
@@ -274,7 +273,7 @@
 *t* must have the same shape as *v*.  For example, consider the following
 definition::
 
-  let pair 't (x: t) (y: t) = (x, y)
+  def pair 't (x: t) (y: t) = (x, y)
 
 The application ``pair [1] [2,3]`` will fail at run-time.
 
@@ -287,16 +286,16 @@
 
 Infix operators are defined much like functions::
 
-  let (p1: t1) op (p2: t2): rt = ...
+  def (p1: t1) op (p2: t2): rt = ...
 
 For example::
 
-  let (a:i32,b:i32) +^ (c:i32,d:i32) = (a+c, b+d)
+  def (a:i32,b:i32) +^ (c:i32,d:i32) = (a+c, b+d)
 
 We can also define operators by enclosing the operator name in
 parentheses and suffixing the parameters, as an ordinary function::
 
-  let (+^) (a:i32,b:i32) (c:i32,d:i32) = (a+c, b+d)
+  def (+^) (a:i32,b:i32) (c:i32,d:i32) = (a+c, b+d)
 
 This is necessary when defining a polymorphic operator.
 
@@ -320,7 +319,7 @@
 An infix operator can also be defined with prefix notation, like an
 ordinary function, by enclosing it in parentheses::
 
-  let (+) (x: i32) (y: i32) = x - y
+  def (+) (x: i32) (y: i32) = x - y
 
 This is necessary when defining operators that take type or shape
 parameters.
@@ -330,7 +329,7 @@
 Entry Points
 ~~~~~~~~~~~~
 
-Apart from declaring a function with the keyword ``let``, it can also
+Apart from declaring a function with the keyword ``def``, it can also
 be declared with ``entry``.  When the Futhark program is compiled any
 top-level function declared with ``entry`` will be exposed as an entry
 point.  If the Futhark program has been compiled as a library, these
@@ -349,7 +348,7 @@
 
 A named value/constant can be declared as follows::
 
-  let name: type = definition
+  def name: type = definition
 
 The definition can be an arbitrary expression, including function
 calls and other values, although they must be in scope before the
@@ -389,7 +388,7 @@
 
   type two_intvecs [n] = ([n]i32, [n]i32)
 
-  let x: two_intvecs [2] = (iota 2, replicate 2 0)
+  def x: two_intvecs [2] = (iota 2, replicate 2 0)
 
 Size parameters work much like shape declarations for arrays.  Like
 shape declarations, they can be elided via square brackets containing
@@ -404,7 +403,7 @@
 
   type two_vecs [n] 't = ([n]t, [n]t)
   type two_intvecs [n] = two_vecs [n] i32
-  let x: two_vecs [2] i32 = (iota 2, replicate 2 0)
+  def x: two_vecs [2] i32 = (iota 2, replicate 2 0)
 
 A *size-lifted type parameter* is prefixed with ``'~``, and a *fully
 lifted type parameter* with ``'^``.  These have the same rules and
@@ -1059,7 +1058,7 @@
 used to express invariants about the shapes of arrays that are
 accepted or produced by the function.  For example::
 
-  let f [n] (a: [n]i32) (b: [n]i32): [n]i32 =
+  def f [n] (a: [n]i32) (b: [n]i32): [n]i32 =
     map2 (+) a b
 
 We use a *size parameter*, ``[n]``, to explicitly quantify sizes.  The
@@ -1082,7 +1081,7 @@
 *Size-dependent types* are supported, as the names of parameters can
 be used in the return type of a function::
 
-  let replicate 't (n: i64) (x: t): [n]t = ...
+  def replicate 't (n: i64) (x: t): [n]t = ...
 
 An application ``replicate 10 0`` will have type ``[10]i32``.
 
@@ -1211,7 +1210,7 @@
 annotations can refer only to variables and constants, this is
 necessary when writing more complicated size functions::
 
-  let concat_to 'a (m: i32) (a: []a) (b: []a) : [m]a =
+  def concat_to 'a (m: i32) (a: []a) (b: []a) : [m]a =
     a ++ b :> [m]a
 
 Only expression-level type annotations give rise to run-time checks.
@@ -1228,11 +1227,11 @@
 any size parameter must be used as the size of some parameter.  This
 is an error::
 
-  let f [n] (x: i32) = n
+  def f [n] (x: i32) = n
 
 The following is not an error::
 
-  let f [n] (g: [n]i32 -> [n]i32) = ...
+  def f [n] (g: [n]i32 -> [n]i32) = ...
 
 However, using this function comes with a constraint: whenever an
 application ``f x`` occurs, the value of the size parameter must be
@@ -1248,7 +1247,7 @@
 parameters whose first use is *not* as a concrete array size.  For
 example, it does not apply to uses of the following function::
 
-  let f [n] (arr: [n]i32) (g: [n]i32 -> [n]i32) = ...
+  def f [n] (arr: [n]i32) (g: [n]i32 -> [n]i32) = ...
 
 This is because the proper value of ``n`` can be read directly from
 the actual size of the array.
@@ -1262,7 +1261,7 @@
 to be the same as the elements of ``b``, but the size of the elements
 of ``b`` are not known at the time ``a`` is constructed::
 
-  let main (b: bool) (xs: []i32) =
+  def main (b: bool) (xs: []i32) =
     let a = [] : [][]i32
     let b = [filter (>0) xs]
     in a[0] == b[0]
@@ -1278,7 +1277,7 @@
 
   type sum = #foo ([]i32) | #bar ([]i32)
 
-  let main (xs: *[]i32) =
+  def main (xs: *[]i32) =
     let v : sum = #foo xs
     in xs
 
@@ -1388,7 +1387,7 @@
 When defining a function parameter or return type, we can mark it as
 *unique* by prefixing it with an asterisk.  For example::
 
-  let modify (a: *[]i32) (i: i32) (x: i32): *[]i32 =
+  def modify (a: *[]i32) (i: i32) (x: i32): *[]i32 =
     a with [i] = a[i] + x
 
 For bulk in-place updates with multiple values, use the ``scatter``
@@ -1478,7 +1477,7 @@
 
   module Vec3 = {
     type t = ( f32 , f32 , f32 )
-    let add(a: t) (b: t): t =
+    def add(a: t) (b: t): t =
       let (a1, a2, a3) = a in
       let (b1, b2, b3) = b in
       (a1 + b1, a2 + b2 , a3 + b3)
@@ -1490,7 +1489,7 @@
 notation::
 
     type vector = Vec3.t
-    let double(v: vector): vector = Vec3.add v v
+    def double(v: vector): vector = Vec3.add v v
 
 We can also use ``open Vec3`` to bring the names defined by ``Vec3``
 into the current scope.  Multiple modules can be opened simultaneously
@@ -1545,7 +1544,7 @@
 modules.  For example::
 
   module Times = \(M: Addable) -> {
-    let times (x: M.t) (k: i32): M.t =
+    def times (x: M.t) (k: i32): M.t =
       loop x' = x for i < k do
         M.add x' x
   }
diff --git a/docs/man/futhark.rst b/docs/man/futhark.rst
--- a/docs/man/futhark.rst
+++ b/docs/man/futhark.rst
@@ -47,6 +47,13 @@
 (e.g. ``#1``) and print it in binary representation to standard
 output.  This does not work for ``script`` datasets.
 
+futhark defs PROGRAM
+--------------------
+
+Print names and locations of every top-level definition in the program
+(including top levels of modules), one per line.  The program need not
+be type-correct, but it must be contain syntax errors.
+
 futhark dev options... PROGRAM
 ------------------------------
 
diff --git a/futhark.cabal b/futhark.cabal
--- a/futhark.cabal
+++ b/futhark.cabal
@@ -1,6 +1,6 @@
 cabal-version: 2.4
 name:           futhark
-version:        0.20.8
+version:        0.21.1
 synopsis:       An optimising compiler for a functional, array-oriented language.
 
 description:    Futhark is a small programming language designed to be compiled to
@@ -80,6 +80,7 @@
       Futhark.CLI.Check
       Futhark.CLI.Datacmp
       Futhark.CLI.Dataset
+      Futhark.CLI.Defs
       Futhark.CLI.Dev
       Futhark.CLI.Doc
       Futhark.CLI.Literate
diff --git a/prelude/array.fut b/prelude/array.fut
--- a/prelude/array.fut
+++ b/prelude/array.fut
@@ -8,53 +8,53 @@
 -- | The size of the outer dimension of an array.
 --
 -- **Complexity:** O(1).
-let length [n] 't (_: [n]t) = n
+def length [n] 't (_: [n]t) = n
 
 -- | Is the array empty?
 --
 -- **Complexity:** O(1).
-let null [n] 't (_: [n]t) = n == 0
+def null [n] 't (_: [n]t) = n == 0
 
 -- | The first element of the array.
 --
 -- **Complexity:** O(1).
-let head [n] 't (x: [n]t) = x[0]
+def head [n] 't (x: [n]t) = x[0]
 
 -- | The last element of the array.
 --
 -- **Complexity:** O(1).
-let last [n] 't (x: [n]t) = x[n-1]
+def last [n] 't (x: [n]t) = x[n-1]
 
 -- | Everything but the first element of the array.
 --
 -- **Complexity:** O(1).
-let tail [n] 't (x: [n]t) = x[1:]
+def tail [n] 't (x: [n]t) = x[1:]
 
 -- | Everything but the last element of the array.
 --
 -- **Complexity:** O(1).
-let init [n] 't (x: [n]t) = x[0:n-1]
+def init [n] 't (x: [n]t) = x[0:n-1]
 
 -- | Take some number of elements from the head of the array.
 --
 -- **Complexity:** O(1).
-let take [n] 't (i: i64) (x: [n]t): [i]t = x[0:i]
+def take [n] 't (i: i64) (x: [n]t): [i]t = x[0:i]
 
 -- | Remove some number of elements from the head of the array.
 --
 -- **Complexity:** O(1).
-let drop [n] 't (i: i64) (x: [n]t) = x[i:]
+def drop [n] 't (i: i64) (x: [n]t) = x[i:]
 
 -- | Split an array at a given position.
 --
 -- **Complexity:** O(1).
-let split [n] 't (i: i64) (xs: [n]t): ([i]t, []t) =
+def split [n] 't (i: i64) (xs: [n]t): ([i]t, []t) =
   (xs[:i] :> [i]t, xs[i:])
 
 -- | Return the elements of the array in reverse order.
 --
 -- **Complexity:** O(1).
-let reverse [n] 't (x: [n]t): [n]t = x[::-1] :> [n]t
+def reverse [n] 't (x: [n]t): [n]t = x[::-1] :> [n]t
 
 -- | Concatenate two arrays.  Warning: never try to perform a reduction
 -- with this operator; it will not work.
@@ -62,15 +62,15 @@
 -- **Work:** O(n).
 --
 -- **Span:** O(1).
-let (++) [n] [m] 't (xs: [n]t) (ys: [m]t): *[]t = intrinsics.concat (xs, ys)
+def (++) [n] [m] 't (xs: [n]t) (ys: [m]t): *[]t = intrinsics.concat (xs, ys)
 
 -- | An old-fashioned way of saying `++`.
-let concat [n] [m] 't (xs: [n]t) (ys: [m]t): *[]t = xs ++ ys
+def concat [n] [m] 't (xs: [n]t) (ys: [m]t): *[]t = xs ++ ys
 
 -- | Concatenation where the result has a predetermined size.  If the
 -- provided size is wrong, the function will fail with a run-time
 -- error.
-let concat_to [n] [m] 't (k: i64) (xs: [n]t) (ys: [m]t): *[k]t = xs ++ ys :> *[k]t
+def concat_to [n] [m] 't (k: i64) (xs: [n]t) (ys: [m]t): *[k]t = xs ++ ys :> *[k]t
 
 -- | Rotate an array some number of elements to the left.  A negative
 -- rotation amount is also supported.
@@ -78,7 +78,7 @@
 -- For example, if `b==rotate r a`, then `b[x] = a[x+r]`.
 --
 -- **Complexity:** O(1).
-let rotate [n] 't (r: i64) (xs: [n]t): [n]t = intrinsics.rotate (r, xs) :> *[n]t
+def rotate [n] 't (r: i64) (xs: [n]t): [n]t = intrinsics.rotate (r, xs) :> *[n]t
 
 -- | Construct an array of consecutive integers of the given length,
 -- starting at 0.
@@ -86,7 +86,7 @@
 -- **Work:** O(n).
 --
 -- **Span:** O(1).
-let iota (n: i64): *[n]i64 =
+def iota (n: i64): *[n]i64 =
   0..1..<n
 
 -- | Construct an array comprising valid indexes into some other
@@ -95,7 +95,7 @@
 -- **Work:** O(n).
 --
 -- **Span:** O(1).
-let indices [n] 't (_: [n]t) : *[n]i64 =
+def indices [n] 't (_: [n]t) : *[n]i64 =
   iota n
 
 -- | Construct an array of the given length containing the given
@@ -104,7 +104,7 @@
 -- **Work:** O(n).
 --
 -- **Span:** O(1).
-let replicate 't (n: i64) (x: t): *[n]t =
+def replicate 't (n: i64) (x: t): *[n]t =
   map (const x) (iota n)
 
 -- | Copy a value.  The result will not alias anything.
@@ -112,46 +112,46 @@
 -- **Work:** O(n).
 --
 -- **Span:** O(1).
-let copy 't (a: t): *t =
+def copy 't (a: t): *t =
   ([a])[0]
 
 -- | Combines the outer two dimensions of an array.
 --
 -- **Complexity:** O(1).
-let flatten [n][m] 't (xs: [n][m]t): []t =
+def flatten [n][m] 't (xs: [n][m]t): []t =
   intrinsics.flatten xs
 
 -- | Like `flatten`@term, but where the final size is known.  Fails at
 -- runtime if the provided size is wrong.
-let flatten_to [n][m] 't (l: i64) (xs: [n][m]t): [l]t =
+def flatten_to [n][m] 't (l: i64) (xs: [n][m]t): [l]t =
   flatten xs :> [l]t
 
 -- | Like `flatten`, but on the outer three dimensions of an array.
-let flatten_3d [n][m][l] 't (xs: [n][m][l]t): []t =
+def flatten_3d [n][m][l] 't (xs: [n][m][l]t): []t =
   flatten (flatten xs)
 
 -- | Like `flatten`, but on the outer four dimensions of an array.
-let flatten_4d [n][m][l][k] 't (xs: [n][m][l][k]t): []t =
+def flatten_4d [n][m][l][k] 't (xs: [n][m][l][k]t): []t =
   flatten (flatten_3d xs)
 
 -- | Splits the outer dimension of an array in two.
 --
 -- **Complexity:** O(1).
-let unflatten [p] 't (n: i64) (m: i64) (xs: [p]t): [n][m]t =
+def unflatten [p] 't (n: i64) (m: i64) (xs: [p]t): [n][m]t =
   intrinsics.unflatten (n, m, xs) :> [n][m]t
 
 -- | Like `unflatten`, but produces three dimensions.
-let unflatten_3d [p] 't (n: i64) (m: i64) (l: i64) (xs: [p]t): [n][m][l]t =
+def unflatten_3d [p] 't (n: i64) (m: i64) (l: i64) (xs: [p]t): [n][m][l]t =
   unflatten n m (unflatten (n*m) l xs)
 
 -- | Like `unflatten`, but produces four dimensions.
-let unflatten_4d [p] 't (n: i64) (m: i64) (l: i64) (k: i64) (xs: [p]t): [n][m][l][k]t =
+def unflatten_4d [p] 't (n: i64) (m: i64) (l: i64) (k: i64) (xs: [p]t): [n][m][l][k]t =
   unflatten n m (unflatten_3d (n*m) l k xs)
 
 -- | Transpose an array.
 --
 -- **Complexity:** O(1).
-let transpose [n] [m] 't (a: [n][m]t): [m][n]t =
+def transpose [n] [m] 't (a: [n][m]t): [m][n]t =
   intrinsics.transpose a :> [m][n]t
 
 -- | True if all of the input elements are true.  Produces true on an
@@ -160,7 +160,7 @@
 -- **Work:** O(n).
 --
 -- **Span:** O(log(n)).
-let and [n] (xs: [n]bool) = all id xs
+def and [n] (xs: [n]bool) = all id xs
 
 -- | True if any of the input elements are true.  Produces false on an
 -- empty array.
@@ -168,14 +168,14 @@
 -- **Work:** O(n).
 --
 -- **Span:** O(log(n)).
-let or [n] (xs: [n]bool) = any id xs
+def or [n] (xs: [n]bool) = any id xs
 
 -- | Perform a *sequential* left-fold of an array.
 --
 -- **Work:** O(n ✕ W(f))).
 --
 -- **Span:** O(n ✕ S(f)).
-let foldl [n] 'a 'b (f: a -> b -> a) (acc: a) (bs: [n]b): a =
+def foldl [n] 'a 'b (f: a -> b -> a) (acc: a) (bs: [n]b): a =
   loop acc for b in bs do f acc b
 
 -- | Perform a *sequential* right-fold of an array.
@@ -183,7 +183,7 @@
 -- **Work:** O(n ✕ W(f))).
 --
 -- **Span:** O(n ✕ S(f)).
-let foldr [n] 'a 'b (f: b -> a -> a) (acc: a) (bs: [n]b): a =
+def foldr [n] 'a 'b (f: b -> a -> a) (acc: a) (bs: [n]b): a =
   foldl (flip f) acc (reverse bs)
 
 -- | Create a value for each point in a one-dimensional index space.
@@ -191,7 +191,7 @@
 -- **Work:** *O(n ✕ W(f))*
 --
 -- **Span:** *O(S(f))*
-let tabulate 'a (n: i64) (f: i64 -> a): *[n]a =
+def tabulate 'a (n: i64) (f: i64 -> a): *[n]a =
   map1 f (iota n)
 
 -- | Create a value for each point in a two-dimensional index space.
@@ -199,7 +199,7 @@
 -- **Work:** *O(n ✕ W(f))*
 --
 -- **Span:** *O(S(f))*
-let tabulate_2d 'a (n: i64) (m: i64) (f: i64 -> i64 -> a): *[n][m]a =
+def tabulate_2d 'a (n: i64) (m: i64) (f: i64 -> i64 -> a): *[n][m]a =
   map1 (f >-> tabulate m) (iota n)
 
 -- | Create a value for each point in a three-dimensional index space.
@@ -207,5 +207,5 @@
 -- **Work:** *O(n ✕ W(f))*
 --
 -- **Span:** *O(S(f))*
-let tabulate_3d 'a (n: i64) (m: i64) (o: i64) (f: i64 -> i64 -> i64 -> a): *[n][m][o]a =
+def tabulate_3d 'a (n: i64) (m: i64) (o: i64) (f: i64 -> i64 -> i64 -> a): *[n][m][o]a =
   map1 (f >-> tabulate_2d m o) (iota n)
diff --git a/prelude/functional.fut b/prelude/functional.fut
--- a/prelude/functional.fut
+++ b/prelude/functional.fut
@@ -6,7 +6,7 @@
 -- ```
 -- x |> f |> g |> h
 -- ```
-let (|>) '^a '^b (x: a) (f: a -> b): b = f x
+def (|>) '^a '^b (x: a) (f: a -> b): b = f x
 
 -- | Right to left application.
 --
@@ -24,7 +24,7 @@
 -- filter (>0) [-1,0,1] |> length
 -- ```
 
-let (<|) '^a '^b (f: a -> b) (x: a) = f x
+def (<|) '^a '^b (f: a -> b) (x: a) = f x
 
 -- | Function composition, with values flowing from left to right.
 --
@@ -36,49 +36,49 @@
 -- ```
 --
 -- In such cases you can use the pipe operator `|>`@term instead.
-let (>->) '^a '^b '^c (f: a -> b) (g: b -> c) (x: a): c = g (f x)
+def (>->) '^a '^b '^c (f: a -> b) (g: b -> c) (x: a): c = g (f x)
 
 -- | Function composition, with values flowing from right to left.
 -- This is the same as the `∘` operator known from mathematics.
 --
 -- Has the same restrictions with respect to anonymous sizes as
 -- `>->`@term.
-let (<-<) '^a '^b '^c (g: b -> c) (f: a -> b) (x: a): c = g (f x)
+def (<-<) '^a '^b '^c (g: b -> c) (f: a -> b) (x: a): c = g (f x)
 
 -- | Flip the arguments passed to a function.
 --
 -- ```
 -- f x y == flip f y x
 -- ```
-let flip '^a '^b '^c (f: a -> b -> c) (b: b) (a: a): c =
+def flip '^a '^b '^c (f: a -> b -> c) (b: b) (a: a): c =
   f a b
 
 -- | Transform a function taking a pair into a function taking two
 -- arguments.
-let curry '^a '^b '^c (f: (a, b) -> c) (a: a) (b: b): c =
+def curry '^a '^b '^c (f: (a, b) -> c) (a: a) (b: b): c =
   f (a, b)
 
 -- | Transform a function taking two arguments in a function taking a
 -- pair.
-let uncurry '^a '^b '^c (f: a -> b -> c) (a: a, b: b): c =
+def uncurry '^a '^b '^c (f: a -> b -> c) (a: a, b: b): c =
   f a b
 
 -- | The constant function.
-let const '^a '^b (x: a) (_: b): a = x
+def const '^a '^b (x: a) (_: b): a = x
 
 -- | The identity function.
-let id '^a (x: a) = x
+def id '^a (x: a) = x
 
 -- | Apply a function some number of times.
-let iterate 'a (n: i32) (f: a -> a) (x: a) =
+def iterate 'a (n: i32) (f: a -> a) (x: a) =
   loop x for _i < n do f x
 
 -- | Keep applying `f` until `p` returns true for the input value.
 -- May apply zero times.  *Note*: may not terminate.
-let iterate_until 'a (p: a -> bool) (f: a -> a) (x: a) =
+def iterate_until 'a (p: a -> bool) (f: a -> a) (x: a) =
   loop x while ! (p x) do f x
 
 -- | Keep applying `f` while `p` returns true for the input value.
 -- May apply zero times.  *Note*: may not terminate.
-let iterate_while 'a (p: a -> bool) (f: a -> a) (x: a) =
+def iterate_while 'a (p: a -> bool) (f: a -> a) (x: a) =
   loop x while p x do f x
diff --git a/prelude/math.fut b/prelude/math.fut
--- a/prelude/math.fut
+++ b/prelude/math.fut
@@ -227,951 +227,951 @@
 module bool: from_prim with t = bool = {
   type t = bool
 
-  let i8  = intrinsics.itob_i8_bool
-  let i16 = intrinsics.itob_i16_bool
-  let i32 = intrinsics.itob_i32_bool
-  let i64 = intrinsics.itob_i64_bool
-
-  let u8  (x: u8)  = intrinsics.itob_i8_bool (intrinsics.sign_i8 x)
-  let u16 (x: u16) = intrinsics.itob_i16_bool (intrinsics.sign_i16 x)
-  let u32 (x: u32) = intrinsics.itob_i32_bool (intrinsics.sign_i32 x)
-  let u64 (x: u64) = intrinsics.itob_i64_bool (intrinsics.sign_i64 x)
-
-  let f16 (x: f16) = x != 0f16
-  let f32 (x: f32) = x != 0f32
-  let f64 (x: f64) = x != 0f64
-
-  let bool (x: bool) = x
-}
-
-module i8: (integral with t = i8) = {
-  type t = i8
-
-  let (x: i8) + (y: i8) = intrinsics.add8 (x, y)
-  let (x: i8) - (y: i8) = intrinsics.sub8 (x, y)
-  let (x: i8) * (y: i8) = intrinsics.mul8 (x, y)
-  let (x: i8) / (y: i8) = intrinsics.sdiv8 (x, y)
-  let (x: i8) ** (y: i8) = intrinsics.pow8 (x, y)
-  let (x: i8) % (y: i8) = intrinsics.smod8 (x, y)
-  let (x: i8) // (y: i8) = intrinsics.squot8 (x, y)
-  let (x: i8) %% (y: i8) = intrinsics.srem8 (x, y)
-
-  let (x: i8) & (y: i8) = intrinsics.and8 (x, y)
-  let (x: i8) | (y: i8) = intrinsics.or8 (x, y)
-  let (x: i8) ^ (y: i8) = intrinsics.xor8 (x, y)
-  let not (x: i8) = intrinsics.complement8 x
-
-  let (x: i8) << (y: i8) = intrinsics.shl8 (x, y)
-  let (x: i8) >> (y: i8) = intrinsics.ashr8 (x, y)
-  let (x: i8) >>> (y: i8) = intrinsics.lshr8 (x, y)
-
-  let i8  (x: i8)  = intrinsics.sext_i8_i8 x
-  let i16 (x: i16) = intrinsics.sext_i16_i8 x
-  let i32 (x: i32) = intrinsics.sext_i32_i8 x
-  let i64 (x: i64) = intrinsics.sext_i64_i8 x
-
-  let u8  (x: u8)  = intrinsics.zext_i8_i8 (intrinsics.sign_i8 x)
-  let u16 (x: u16) = intrinsics.zext_i16_i8 (intrinsics.sign_i16 x)
-  let u32 (x: u32) = intrinsics.zext_i32_i8 (intrinsics.sign_i32 x)
-  let u64 (x: u64) = intrinsics.zext_i64_i8 (intrinsics.sign_i64 x)
-
-  let f16 (x: f16) = intrinsics.fptosi_f16_i8 x
-  let f32 (x: f32) = intrinsics.fptosi_f32_i8 x
-  let f64 (x: f64) = intrinsics.fptosi_f64_i8 x
-
-  let bool = intrinsics.btoi_bool_i8
-
-  let to_i32(x: i8) = intrinsics.sext_i8_i32 x
-  let to_i64(x: i8) = intrinsics.sext_i8_i64 x
-
-  let (x: i8) == (y: i8) = intrinsics.eq_i8 (x, y)
-  let (x: i8) < (y: i8) = intrinsics.slt8 (x, y)
-  let (x: i8) > (y: i8) = intrinsics.slt8 (y, x)
-  let (x: i8) <= (y: i8) = intrinsics.sle8 (x, y)
-  let (x: i8) >= (y: i8) = intrinsics.sle8 (y, x)
-  let (x: i8) != (y: i8) = !(x == y)
-
-  let sgn (x: i8) = intrinsics.ssignum8 x
-  let abs (x: i8) = intrinsics.abs8 x
-
-  let neg (x: t) = -x
-  let max (x: t) (y: t) = intrinsics.smax8 (x, y)
-  let min (x: t) (y: t) = intrinsics.smin8 (x, y)
-
-  let highest = 127i8
-  let lowest = highest + 1i8
-
-  let num_bits = 8i32
-  let get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
-  let set_bit (bit: i32) (x: t) (b: i32) =
-    ((x & i32 (!(1 intrinsics.<< bit))) | i32 (b intrinsics.<< bit))
-  let popc = intrinsics.popc8
-  let mul_hi a b = intrinsics.mul_hi8 (i8 a, i8 b)
-  let mad_hi a b c = intrinsics.mad_hi8 (i8 a, i8 b, i8 c)
-  let clz = intrinsics.clz8
-  let ctz = intrinsics.ctz8
-
-  let sum = reduce (+) (i32 0)
-  let product = reduce (*) (i32 1)
-  let maximum = reduce max lowest
-  let minimum = reduce min highest
-}
-
-module i16: (integral with t = i16) = {
-  type t = i16
-
-  let (x: i16) + (y: i16) = intrinsics.add16 (x, y)
-  let (x: i16) - (y: i16) = intrinsics.sub16 (x, y)
-  let (x: i16) * (y: i16) = intrinsics.mul16 (x, y)
-  let (x: i16) / (y: i16) = intrinsics.sdiv16 (x, y)
-  let (x: i16) ** (y: i16) = intrinsics.pow16 (x, y)
-  let (x: i16) % (y: i16) = intrinsics.smod16 (x, y)
-  let (x: i16) // (y: i16) = intrinsics.squot16 (x, y)
-  let (x: i16) %% (y: i16) = intrinsics.srem16 (x, y)
-
-  let (x: i16) & (y: i16) = intrinsics.and16 (x, y)
-  let (x: i16) | (y: i16) = intrinsics.or16 (x, y)
-  let (x: i16) ^ (y: i16) = intrinsics.xor16 (x, y)
-  let not (x: i16) = intrinsics.complement16 x
-
-  let (x: i16) << (y: i16) = intrinsics.shl16 (x, y)
-  let (x: i16) >> (y: i16) = intrinsics.ashr16 (x, y)
-  let (x: i16) >>> (y: i16) = intrinsics.lshr16 (x, y)
-
-  let i8  (x: i8)  = intrinsics.sext_i8_i16 x
-  let i16 (x: i16) = intrinsics.sext_i16_i16 x
-  let i32 (x: i32) = intrinsics.sext_i32_i16 x
-  let i64 (x: i64) = intrinsics.sext_i64_i16 x
-
-  let u8  (x: u8)  = intrinsics.zext_i8_i16 (intrinsics.sign_i8 x)
-  let u16 (x: u16) = intrinsics.zext_i16_i16 (intrinsics.sign_i16 x)
-  let u32 (x: u32) = intrinsics.zext_i32_i16 (intrinsics.sign_i32 x)
-  let u64 (x: u64) = intrinsics.zext_i64_i16 (intrinsics.sign_i64 x)
-
-  let f16 (x: f16) = intrinsics.fptosi_f16_i16 x
-  let f32 (x: f32) = intrinsics.fptosi_f32_i16 x
-  let f64 (x: f64) = intrinsics.fptosi_f64_i16 x
-
-  let bool = intrinsics.btoi_bool_i16
-
-  let to_i32(x: i16) = intrinsics.sext_i16_i32 x
-  let to_i64(x: i16) = intrinsics.sext_i16_i64 x
-
-  let (x: i16) == (y: i16) = intrinsics.eq_i16 (x, y)
-  let (x: i16) < (y: i16) = intrinsics.slt16 (x, y)
-  let (x: i16) > (y: i16) = intrinsics.slt16 (y, x)
-  let (x: i16) <= (y: i16) = intrinsics.sle16 (x, y)
-  let (x: i16) >= (y: i16) = intrinsics.sle16 (y, x)
-  let (x: i16) != (y: i16) = !(x == y)
-
-  let sgn (x: i16) = intrinsics.ssignum16 x
-  let abs (x: i16) = intrinsics.abs16 x
-
-  let neg (x: t) = -x
-  let max (x: t) (y: t) = intrinsics.smax16 (x, y)
-  let min (x: t) (y: t) = intrinsics.smin16 (x, y)
-
-  let highest = 32767i16
-  let lowest = highest + 1i16
-
-  let num_bits = 16i32
-  let get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
-  let set_bit (bit: i32) (x: t) (b: i32) =
-    ((x & i32 (!(1 intrinsics.<< bit))) | i32 (b intrinsics.<< bit))
-  let popc = intrinsics.popc16
-  let mul_hi a b = intrinsics.mul_hi16 (i16 a, i16 b)
-  let mad_hi a b c = intrinsics.mad_hi16 (i16 a, i16 b, i16 c)
-  let clz = intrinsics.clz16
-  let ctz = intrinsics.ctz16
-
-  let sum = reduce (+) (i32 0)
-  let product = reduce (*) (i32 1)
-  let maximum = reduce max lowest
-  let minimum = reduce min highest
-}
-
-module i32: (integral with t = i32) = {
-  type t = i32
-
-  let sign (x: u32) = intrinsics.sign_i32 x
-  let unsign (x: i32) = intrinsics.unsign_i32 x
-
-  let (x: i32) + (y: i32) = intrinsics.add32 (x, y)
-  let (x: i32) - (y: i32) = intrinsics.sub32 (x, y)
-  let (x: i32) * (y: i32) = intrinsics.mul32 (x, y)
-  let (x: i32) / (y: i32) = intrinsics.sdiv32 (x, y)
-  let (x: i32) ** (y: i32) = intrinsics.pow32 (x, y)
-  let (x: i32) % (y: i32) = intrinsics.smod32 (x, y)
-  let (x: i32) // (y: i32) = intrinsics.squot32 (x, y)
-  let (x: i32) %% (y: i32) = intrinsics.srem32 (x, y)
-
-  let (x: i32) & (y: i32) = intrinsics.and32 (x, y)
-  let (x: i32) | (y: i32) = intrinsics.or32 (x, y)
-  let (x: i32) ^ (y: i32) = intrinsics.xor32 (x, y)
-  let not (x: i32) = intrinsics.complement32 x
-
-  let (x: i32) << (y: i32) = intrinsics.shl32 (x, y)
-  let (x: i32) >> (y: i32) = intrinsics.ashr32 (x, y)
-  let (x: i32) >>> (y: i32) = intrinsics.lshr32 (x, y)
-
-  let i8  (x: i8)  = intrinsics.sext_i8_i32 x
-  let i16 (x: i16) = intrinsics.sext_i16_i32 x
-  let i32 (x: i32) = intrinsics.sext_i32_i32 x
-  let i64 (x: i64) = intrinsics.sext_i64_i32 x
-
-  let u8  (x: u8)  = intrinsics.zext_i8_i32 (intrinsics.sign_i8 x)
-  let u16 (x: u16) = intrinsics.zext_i16_i32 (intrinsics.sign_i16 x)
-  let u32 (x: u32) = intrinsics.zext_i32_i32 (intrinsics.sign_i32 x)
-  let u64 (x: u64) = intrinsics.zext_i64_i32 (intrinsics.sign_i64 x)
-
-  let f16 (x: f16) = intrinsics.fptosi_f16_i32 x
-  let f32 (x: f32) = intrinsics.fptosi_f32_i32 x
-  let f64 (x: f64) = intrinsics.fptosi_f64_i32 x
-
-  let bool = intrinsics.btoi_bool_i32
-
-  let to_i32(x: i32) = intrinsics.sext_i32_i32 x
-  let to_i64(x: i32) = intrinsics.sext_i32_i64 x
-
-  let (x: i32) == (y: i32) = intrinsics.eq_i32 (x, y)
-  let (x: i32) < (y: i32) = intrinsics.slt32 (x, y)
-  let (x: i32) > (y: i32) = intrinsics.slt32 (y, x)
-  let (x: i32) <= (y: i32) = intrinsics.sle32 (x, y)
-  let (x: i32) >= (y: i32) = intrinsics.sle32 (y, x)
-  let (x: i32) != (y: i32) = !(x == y)
-
-  let sgn (x: i32) = intrinsics.ssignum32 x
-  let abs (x: i32) = intrinsics.abs32 x
-
-  let neg (x: t) = -x
-  let max (x: t) (y: t) = intrinsics.smax32 (x, y)
-  let min (x: t) (y: t) = intrinsics.smin32 (x, y)
-
-  let highest = 2147483647i32
-  let lowest = highest + 1
-
-  let num_bits = 32i32
-  let get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
-  let set_bit (bit: i32) (x: t) (b: i32) =
-    ((x & i32 (!(1 intrinsics.<< bit))) | i32 (b intrinsics.<< bit))
-  let popc = intrinsics.popc32
-  let mul_hi a b = intrinsics.mul_hi32 (i32 a, i32 b)
-  let mad_hi a b c = intrinsics.mad_hi32 (i32 a, i32 b, i32 c)
-  let clz = intrinsics.clz32
-  let ctz = intrinsics.ctz32
-
-  let sum = reduce (+) (i32 0)
-  let product = reduce (*) (i32 1)
-  let maximum = reduce max lowest
-  let minimum = reduce min highest
-}
-
-module i64: (integral with t = i64) = {
-  type t = i64
-
-  let sign (x: u64) = intrinsics.sign_i64 x
-  let unsign (x: i64) = intrinsics.unsign_i64 x
-
-  let (x: i64) + (y: i64) = intrinsics.add64 (x, y)
-  let (x: i64) - (y: i64) = intrinsics.sub64 (x, y)
-  let (x: i64) * (y: i64) = intrinsics.mul64 (x, y)
-  let (x: i64) / (y: i64) = intrinsics.sdiv64 (x, y)
-  let (x: i64) ** (y: i64) = intrinsics.pow64 (x, y)
-  let (x: i64) % (y: i64) = intrinsics.smod64 (x, y)
-  let (x: i64) // (y: i64) = intrinsics.squot64 (x, y)
-  let (x: i64) %% (y: i64) = intrinsics.srem64 (x, y)
-
-  let (x: i64) & (y: i64) = intrinsics.and64 (x, y)
-  let (x: i64) | (y: i64) = intrinsics.or64 (x, y)
-  let (x: i64) ^ (y: i64) = intrinsics.xor64 (x, y)
-  let not (x: i64) = intrinsics.complement64 x
-
-  let (x: i64) << (y: i64) = intrinsics.shl64 (x, y)
-  let (x: i64) >> (y: i64) = intrinsics.ashr64 (x, y)
-  let (x: i64) >>> (y: i64) = intrinsics.lshr64 (x, y)
-
-  let i8  (x: i8)  = intrinsics.sext_i8_i64 x
-  let i16 (x: i16) = intrinsics.sext_i16_i64 x
-  let i32 (x: i32) = intrinsics.sext_i32_i64 x
-  let i64 (x: i64) = intrinsics.sext_i64_i64 x
-
-  let u8  (x: u8)  = intrinsics.zext_i8_i64 (intrinsics.sign_i8 x)
-  let u16 (x: u16) = intrinsics.zext_i16_i64 (intrinsics.sign_i16 x)
-  let u32 (x: u32) = intrinsics.zext_i32_i64 (intrinsics.sign_i32 x)
-  let u64 (x: u64) = intrinsics.zext_i64_i64 (intrinsics.sign_i64 x)
-
-  let f16 (x: f16) = intrinsics.fptosi_f16_i64 x
-  let f32 (x: f32) = intrinsics.fptosi_f32_i64 x
-  let f64 (x: f64) = intrinsics.fptosi_f64_i64 x
-
-  let bool = intrinsics.btoi_bool_i64
-
-  let to_i32(x: i64) = intrinsics.sext_i64_i32 x
-  let to_i64(x: i64) = intrinsics.sext_i64_i64 x
-
-  let (x: i64) == (y: i64) = intrinsics.eq_i64 (x, y)
-  let (x: i64) < (y: i64) = intrinsics.slt64 (x, y)
-  let (x: i64) > (y: i64) = intrinsics.slt64 (y, x)
-  let (x: i64) <= (y: i64) = intrinsics.sle64 (x, y)
-  let (x: i64) >= (y: i64) = intrinsics.sle64 (y, x)
-  let (x: i64) != (y: i64) = !(x == y)
-
-  let sgn (x: i64) = intrinsics.ssignum64 x
-  let abs (x: i64) = intrinsics.abs64 x
-
-  let neg (x: t) = -x
-  let max (x: t) (y: t) = intrinsics.smax64 (x, y)
-  let min (x: t) (y: t) = intrinsics.smin64 (x, y)
-
-  let highest = 9223372036854775807i64
-  let lowest = highest + 1i64
-
-  let num_bits = 64i32
-  let get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
-  let set_bit (bit: i32) (x: t) (b: i32) =
-    ((x & i32 (!(1 intrinsics.<< bit))) | intrinsics.zext_i32_i64 (b intrinsics.<< bit))
-  let popc = intrinsics.popc64
-  let mul_hi a b = intrinsics.mul_hi64 (i64 a, i64 b)
-  let mad_hi a b c = intrinsics.mad_hi64 (i64 a, i64 b, i64 c)
-  let clz = intrinsics.clz64
-  let ctz = intrinsics.ctz64
-
-  let sum = reduce (+) (i32 0)
-  let product = reduce (*) (i32 1)
-  let maximum = reduce max lowest
-  let minimum = reduce min highest
-}
-
-module u8: (integral with t = u8) = {
-  type t = u8
-
-  let sign (x: u8) = intrinsics.sign_i8 x
-  let unsign (x: i8) = intrinsics.unsign_i8 x
-
-  let (x: u8) + (y: u8) = unsign (intrinsics.add8 (sign x, sign y))
-  let (x: u8) - (y: u8) = unsign (intrinsics.sub8 (sign x, sign y))
-  let (x: u8) * (y: u8) = unsign (intrinsics.mul8 (sign x, sign y))
-  let (x: u8) / (y: u8) = unsign (intrinsics.udiv8 (sign x, sign y))
-  let (x: u8) ** (y: u8) = unsign (intrinsics.pow8 (sign x, sign y))
-  let (x: u8) % (y: u8) = unsign (intrinsics.umod8 (sign x, sign y))
-  let (x: u8) // (y: u8) = unsign (intrinsics.udiv8 (sign x, sign y))
-  let (x: u8) %% (y: u8) = unsign (intrinsics.umod8 (sign x, sign y))
-
-  let (x: u8) & (y: u8) = unsign (intrinsics.and8 (sign x, sign y))
-  let (x: u8) | (y: u8) = unsign (intrinsics.or8 (sign x, sign y))
-  let (x: u8) ^ (y: u8) = unsign (intrinsics.xor8 (sign x, sign y))
-  let not (x: u8) = unsign (intrinsics.complement8 (sign x))
-
-  let (x: u8) << (y: u8) = unsign (intrinsics.shl8 (sign x, sign y))
-  let (x: u8) >> (y: u8) = unsign (intrinsics.ashr8 (sign x, sign y))
-  let (x: u8) >>> (y: u8) = unsign (intrinsics.lshr8 (sign x, sign y))
-
-  let u8  (x: u8)  = unsign (i8.u8 x)
-  let u16 (x: u16) = unsign (i8.u16 x)
-  let u32 (x: u32) = unsign (i8.u32 x)
-  let u64 (x: u64) = unsign (i8.u64 x)
-
-  let i8  (x: i8)  = unsign (intrinsics.zext_i8_i8 x)
-  let i16 (x: i16) = unsign (intrinsics.zext_i16_i8 x)
-  let i32 (x: i32) = unsign (intrinsics.zext_i32_i8 x)
-  let i64 (x: i64) = unsign (intrinsics.zext_i64_i8 x)
-
-  let f16 (x: f16) = unsign (intrinsics.fptoui_f16_i8 x)
-  let f32 (x: f32) = unsign (intrinsics.fptoui_f32_i8 x)
-  let f64 (x: f64) = unsign (intrinsics.fptoui_f64_i8 x)
-
-  let bool x = unsign (intrinsics.btoi_bool_i8 x)
-
-  let to_i32(x: u8) = intrinsics.zext_i8_i32 (sign x)
-  let to_i64(x: u8) = intrinsics.zext_i8_i64 (sign x)
-
-  let (x: u8) == (y: u8) = intrinsics.eq_i8 (sign x, sign y)
-  let (x: u8) < (y: u8) = intrinsics.ult8 (sign x, sign y)
-  let (x: u8) > (y: u8) = intrinsics.ult8 (sign y, sign x)
-  let (x: u8) <= (y: u8) = intrinsics.ule8 (sign x, sign y)
-  let (x: u8) >= (y: u8) = intrinsics.ule8 (sign y, sign x)
-  let (x: u8) != (y: u8) = !(x == y)
-
-  let sgn (x: u8) = unsign (intrinsics.usignum8 (sign x))
-  let abs (x: u8) = x
-
-  let neg (x: t) = -x
-  let max (x: t) (y: t) = unsign (intrinsics.umax8 (sign x, sign y))
-  let min (x: t) (y: t) = unsign (intrinsics.umin8 (sign x, sign y))
-
-  let highest = 255u8
-  let lowest = 0u8
-
-  let num_bits = 8i32
-  let get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
-  let set_bit (bit: i32) (x: t) (b: i32) =
-    ((x & i32 (!(1 intrinsics.<< bit))) | i32 (b intrinsics.<< bit))
-  let popc x = intrinsics.popc8 (sign x)
-  let mul_hi a b = unsign (intrinsics.mul_hi8 (sign a, sign b))
-  let mad_hi a b c = unsign (intrinsics.mad_hi8 (sign a, sign b, sign c))
-  let clz x = intrinsics.clz8 (sign x)
-  let ctz x = intrinsics.ctz8 (sign x)
-
-  let sum = reduce (+) (i32 0)
-  let product = reduce (*) (i32 1)
-  let maximum = reduce max lowest
-  let minimum = reduce min highest
-}
-
-module u16: (integral with t = u16) = {
-  type t = u16
-
-  let sign (x: u16) = intrinsics.sign_i16 x
-  let unsign (x: i16) = intrinsics.unsign_i16 x
-
-  let (x: u16) + (y: u16) = unsign (intrinsics.add16 (sign x, sign y))
-  let (x: u16) - (y: u16) = unsign (intrinsics.sub16 (sign x, sign y))
-  let (x: u16) * (y: u16) = unsign (intrinsics.mul16 (sign x, sign y))
-  let (x: u16) / (y: u16) = unsign (intrinsics.udiv16 (sign x, sign y))
-  let (x: u16) ** (y: u16) = unsign (intrinsics.pow16 (sign x, sign y))
-  let (x: u16) % (y: u16) = unsign (intrinsics.umod16 (sign x, sign y))
-  let (x: u16) // (y: u16) = unsign (intrinsics.udiv16 (sign x, sign y))
-  let (x: u16) %% (y: u16) = unsign (intrinsics.umod16 (sign x, sign y))
-
-  let (x: u16) & (y: u16) = unsign (intrinsics.and16 (sign x, sign y))
-  let (x: u16) | (y: u16) = unsign (intrinsics.or16 (sign x, sign y))
-  let (x: u16) ^ (y: u16) = unsign (intrinsics.xor16 (sign x, sign y))
-  let not (x: u16) = unsign (intrinsics.complement16 (sign x))
-
-  let (x: u16) << (y: u16) = unsign (intrinsics.shl16 (sign x, sign y))
-  let (x: u16) >> (y: u16) = unsign (intrinsics.ashr16 (sign x, sign y))
-  let (x: u16) >>> (y: u16) = unsign (intrinsics.lshr16 (sign x, sign y))
-
-  let u8  (x: u8)  = unsign (i16.u8 x)
-  let u16 (x: u16) = unsign (i16.u16 x)
-  let u32 (x: u32) = unsign (i16.u32 x)
-  let u64 (x: u64) = unsign (i16.u64 x)
-
-  let i8  (x: i8)  = unsign (intrinsics.zext_i8_i16 x)
-  let i16 (x: i16) = unsign (intrinsics.zext_i16_i16 x)
-  let i32 (x: i32) = unsign (intrinsics.zext_i32_i16 x)
-  let i64 (x: i64) = unsign (intrinsics.zext_i64_i16 x)
-
-  let f16 (x: f16) = unsign (intrinsics.fptoui_f16_i16 x)
-  let f32 (x: f32) = unsign (intrinsics.fptoui_f32_i16 x)
-  let f64 (x: f64) = unsign (intrinsics.fptoui_f64_i16 x)
-
-  let bool x = unsign (intrinsics.btoi_bool_i16 x)
-
-  let to_i32(x: u16) = intrinsics.zext_i16_i32 (sign x)
-  let to_i64(x: u16) = intrinsics.zext_i16_i64 (sign x)
-
-  let (x: u16) == (y: u16) = intrinsics.eq_i16 (sign x, sign y)
-  let (x: u16) < (y: u16) = intrinsics.ult16 (sign x, sign y)
-  let (x: u16) > (y: u16) = intrinsics.ult16 (sign y, sign x)
-  let (x: u16) <= (y: u16) = intrinsics.ule16 (sign x, sign y)
-  let (x: u16) >= (y: u16) = intrinsics.ule16 (sign y, sign x)
-  let (x: u16) != (y: u16) = !(x == y)
-
-  let sgn (x: u16) = unsign (intrinsics.usignum16 (sign x))
-  let abs (x: u16) = x
-
-  let neg (x: t) = -x
-  let max (x: t) (y: t) = unsign (intrinsics.umax16 (sign x, sign y))
-  let min (x: t) (y: t) = unsign (intrinsics.umin16 (sign x, sign y))
-
-  let highest = 65535u16
-  let lowest = 0u16
-
-  let num_bits = 16i32
-  let get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
-  let set_bit (bit: i32) (x: t) (b: i32) =
-    ((x & i32 (!(1 intrinsics.<< bit))) | i32 (b intrinsics.<< bit))
-  let popc x = intrinsics.popc16 (sign x)
-  let mul_hi a b = unsign (intrinsics.mul_hi16 (sign a, sign b))
-  let mad_hi a b c = unsign (intrinsics.mad_hi16 (sign a, sign b, sign c))
-  let clz x = intrinsics.clz16 (sign x)
-  let ctz x = intrinsics.ctz16 (sign x)
-
-  let sum = reduce (+) (i32 0)
-  let product = reduce (*) (i32 1)
-  let maximum = reduce max lowest
-  let minimum = reduce min highest
-}
-
-module u32: (integral with t = u32) = {
-  type t = u32
-
-  let sign (x: u32) = intrinsics.sign_i32 x
-  let unsign (x: i32) = intrinsics.unsign_i32 x
-
-  let (x: u32) + (y: u32) = unsign (intrinsics.add32 (sign x, sign y))
-  let (x: u32) - (y: u32) = unsign (intrinsics.sub32 (sign x, sign y))
-  let (x: u32) * (y: u32) = unsign (intrinsics.mul32 (sign x, sign y))
-  let (x: u32) / (y: u32) = unsign (intrinsics.udiv32 (sign x, sign y))
-  let (x: u32) ** (y: u32) = unsign (intrinsics.pow32 (sign x, sign y))
-  let (x: u32) % (y: u32) = unsign (intrinsics.umod32 (sign x, sign y))
-  let (x: u32) // (y: u32) = unsign (intrinsics.udiv32 (sign x, sign y))
-  let (x: u32) %% (y: u32) = unsign (intrinsics.umod32 (sign x, sign y))
-
-  let (x: u32) & (y: u32) = unsign (intrinsics.and32 (sign x, sign y))
-  let (x: u32) | (y: u32) = unsign (intrinsics.or32 (sign x, sign y))
-  let (x: u32) ^ (y: u32) = unsign (intrinsics.xor32 (sign x, sign y))
-  let not (x: u32) = unsign (intrinsics.complement32 (sign x))
-
-  let (x: u32) << (y: u32) = unsign (intrinsics.shl32 (sign x, sign y))
-  let (x: u32) >> (y: u32) = unsign (intrinsics.ashr32 (sign x, sign y))
-  let (x: u32) >>> (y: u32) = unsign (intrinsics.lshr32 (sign x, sign y))
-
-  let u8  (x: u8)  = unsign (i32.u8 x)
-  let u16 (x: u16) = unsign (i32.u16 x)
-  let u32 (x: u32) = unsign (i32.u32 x)
-  let u64 (x: u64) = unsign (i32.u64 x)
-
-  let i8  (x: i8)  = unsign (intrinsics.zext_i8_i32 x)
-  let i16 (x: i16) = unsign (intrinsics.zext_i16_i32 x)
-  let i32 (x: i32) = unsign (intrinsics.zext_i32_i32 x)
-  let i64 (x: i64) = unsign (intrinsics.zext_i64_i32 x)
-
-  let f16 (x: f16) = unsign (intrinsics.fptoui_f16_i32 x)
-  let f32 (x: f32) = unsign (intrinsics.fptoui_f32_i32 x)
-  let f64 (x: f64) = unsign (intrinsics.fptoui_f64_i32 x)
-
-  let bool x = unsign (intrinsics.btoi_bool_i32 x)
-
-  let to_i32(x: u32) = intrinsics.zext_i32_i32 (sign x)
-  let to_i64(x: u32) = intrinsics.zext_i32_i64 (sign x)
-
-  let (x: u32) == (y: u32) = intrinsics.eq_i32 (sign x, sign y)
-  let (x: u32) < (y: u32) = intrinsics.ult32 (sign x, sign y)
-  let (x: u32) > (y: u32) = intrinsics.ult32 (sign y, sign x)
-  let (x: u32) <= (y: u32) = intrinsics.ule32 (sign x, sign y)
-  let (x: u32) >= (y: u32) = intrinsics.ule32 (sign y, sign x)
-  let (x: u32) != (y: u32) = !(x == y)
-
-  let sgn (x: u32) = unsign (intrinsics.usignum32 (sign x))
-  let abs (x: u32) = x
-
-  let highest = 4294967295u32
-  let lowest = highest + 1u32
-
-  let neg (x: t) = -x
-  let max (x: t) (y: t) = unsign (intrinsics.umax32 (sign x, sign y))
-  let min (x: t) (y: t) = unsign (intrinsics.umin32 (sign x, sign y))
-
-  let num_bits = 32i32
-  let get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
-  let set_bit (bit: i32) (x: t) (b: i32) =
-    ((x & i32 (!(1 intrinsics.<< bit))) | i32 (b intrinsics.<< bit))
-  let popc x = intrinsics.popc32 (sign x)
-  let mul_hi a b = unsign (intrinsics.mul_hi32 (sign a, sign b))
-  let mad_hi a b c = unsign (intrinsics.mad_hi32 (sign a, sign b, sign c))
-  let clz x = intrinsics.clz32 (sign x)
-  let ctz x = intrinsics.ctz32 (sign x)
-
-  let sum = reduce (+) (i32 0)
-  let product = reduce (*) (i32 1)
-  let maximum = reduce max lowest
-  let minimum = reduce min highest
-}
-
-module u64: (integral with t = u64) = {
-  type t = u64
-
-  let sign (x: u64) = intrinsics.sign_i64 x
-  let unsign (x: i64) = intrinsics.unsign_i64 x
-
-  let (x: u64) + (y: u64) = unsign (intrinsics.add64 (sign x, sign y))
-  let (x: u64) - (y: u64) = unsign (intrinsics.sub64 (sign x, sign y))
-  let (x: u64) * (y: u64) = unsign (intrinsics.mul64 (sign x, sign y))
-  let (x: u64) / (y: u64) = unsign (intrinsics.udiv64 (sign x, sign y))
-  let (x: u64) ** (y: u64) = unsign (intrinsics.pow64 (sign x, sign y))
-  let (x: u64) % (y: u64) = unsign (intrinsics.umod64 (sign x, sign y))
-  let (x: u64) // (y: u64) = unsign (intrinsics.udiv64 (sign x, sign y))
-  let (x: u64) %% (y: u64) = unsign (intrinsics.umod64 (sign x, sign y))
-
-  let (x: u64) & (y: u64) = unsign (intrinsics.and64 (sign x, sign y))
-  let (x: u64) | (y: u64) = unsign (intrinsics.or64 (sign x, sign y))
-  let (x: u64) ^ (y: u64) = unsign (intrinsics.xor64 (sign x, sign y))
-  let not (x: u64) = unsign (intrinsics.complement64 (sign x))
-
-  let (x: u64) << (y: u64) = unsign (intrinsics.shl64 (sign x, sign y))
-  let (x: u64) >> (y: u64) = unsign (intrinsics.ashr64 (sign x, sign y))
-  let (x: u64) >>> (y: u64) = unsign (intrinsics.lshr64 (sign x, sign y))
-
-  let u8  (x: u8)  = unsign (i64.u8 x)
-  let u16 (x: u16) = unsign (i64.u16 x)
-  let u32 (x: u32) = unsign (i64.u32 x)
-  let u64 (x: u64) = unsign (i64.u64 x)
-
-  let i8 (x: i8)   = unsign (intrinsics.zext_i8_i64 x)
-  let i16 (x: i16) = unsign (intrinsics.zext_i16_i64 x)
-  let i32 (x: i32) = unsign (intrinsics.zext_i32_i64 x)
-  let i64 (x: i64) = unsign (intrinsics.zext_i64_i64 x)
-
-  let f16 (x: f16) = unsign (intrinsics.fptoui_f16_i64 x)
-  let f32 (x: f32) = unsign (intrinsics.fptoui_f32_i64 x)
-  let f64 (x: f64) = unsign (intrinsics.fptoui_f64_i64 x)
-
-  let bool x = unsign (intrinsics.btoi_bool_i64 x)
-
-  let to_i32(x: u64) = intrinsics.zext_i64_i32 (sign x)
-  let to_i64(x: u64) = intrinsics.zext_i64_i64 (sign x)
-
-  let (x: u64) == (y: u64) = intrinsics.eq_i64 (sign x, sign y)
-  let (x: u64) < (y: u64) = intrinsics.ult64 (sign x, sign y)
-  let (x: u64) > (y: u64) = intrinsics.ult64 (sign y, sign x)
-  let (x: u64) <= (y: u64) = intrinsics.ule64 (sign x, sign y)
-  let (x: u64) >= (y: u64) = intrinsics.ule64 (sign y, sign x)
-  let (x: u64) != (y: u64) = !(x == y)
-
-  let sgn (x: u64) = unsign (intrinsics.usignum64 (sign x))
-  let abs (x: u64) = x
-
-  let neg (x: t) = -x
-  let max (x: t) (y: t) = unsign (intrinsics.umax64 (sign x, sign y))
-  let min (x: t) (y: t) = unsign (intrinsics.umin64 (sign x, sign y))
-
-  let highest = 18446744073709551615u64
-  let lowest = highest + 1u64
-
-  let num_bits = 64i32
-  let get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
-  let set_bit (bit: i32) (x: t) (b: i32) =
-    ((x & i32 (!(1 intrinsics.<< bit))) | i32 (b intrinsics.<< bit))
-  let popc x = intrinsics.popc64 (sign x)
-  let mul_hi a b = unsign (intrinsics.mul_hi64 (sign a, sign b))
-  let mad_hi a b c = unsign (intrinsics.mad_hi64 (sign a, sign b, sign c))
-  let clz x = intrinsics.clz64 (sign x)
-  let ctz x = intrinsics.ctz64 (sign x)
-
-  let sum = reduce (+) (i32 0)
-  let product = reduce (*) (i32 1)
-  let maximum = reduce max lowest
-  let minimum = reduce min highest
-}
-
-module f64: (float with t = f64 with int_t = u64) = {
-  type t = f64
-  type int_t = u64
-
-  module i64m = i64
-  module u64m = u64
-
-  let (x: f64) + (y: f64) = intrinsics.fadd64 (x, y)
-  let (x: f64) - (y: f64) = intrinsics.fsub64 (x, y)
-  let (x: f64) * (y: f64) = intrinsics.fmul64 (x, y)
-  let (x: f64) / (y: f64) = intrinsics.fdiv64 (x, y)
-  let (x: f64) % (y: f64) = intrinsics.fmod64 (x, y)
-  let (x: f64) ** (y: f64) = intrinsics.fpow64 (x, y)
-
-  let u8  (x: u8)  = intrinsics.uitofp_i8_f64  (i8.u8 x)
-  let u16 (x: u16) = intrinsics.uitofp_i16_f64 (i16.u16 x)
-  let u32 (x: u32) = intrinsics.uitofp_i32_f64 (i32.u32 x)
-  let u64 (x: u64) = intrinsics.uitofp_i64_f64 (i64.u64 x)
-
-  let i8 (x: i8) = intrinsics.sitofp_i8_f64 x
-  let i16 (x: i16) = intrinsics.sitofp_i16_f64 x
-  let i32 (x: i32) = intrinsics.sitofp_i32_f64 x
-  let i64 (x: i64) = intrinsics.sitofp_i64_f64 x
-
-  let f16 (x: f16) = intrinsics.fpconv_f16_f64 x
-  let f32 (x: f32) = intrinsics.fpconv_f32_f64 x
-  let f64 (x: f64) = intrinsics.fpconv_f64_f64 x
-
-  let bool (x: bool) = if x then 1f64 else 0f64
-
-  let from_fraction (x: i64) (y: i64) = i64 x / i64 y
-  let to_i64 (x: f64) = intrinsics.fptosi_f64_i64 x
-  let to_f64 (x: f64) = x
-
-  let (x: f64) == (y: f64) = intrinsics.eq_f64 (x, y)
-  let (x: f64) < (y: f64) = intrinsics.lt64 (x, y)
-  let (x: f64) > (y: f64) = intrinsics.lt64 (y, x)
-  let (x: f64) <= (y: f64) = intrinsics.le64 (x, y)
-  let (x: f64) >= (y: f64) = intrinsics.le64 (y, x)
-  let (x: f64) != (y: f64) = !(x == y)
-
-  let neg (x: t) = -x
-  let recip (x: t) = 1/x
-  let max (x: t) (y: t) = intrinsics.fmax64 (x, y)
-  let min (x: t) (y: t) = intrinsics.fmin64 (x, y)
-
-  let sgn (x: f64) = intrinsics.fsignum64 x
-  let abs (x: f64) = intrinsics.fabs64 x
-
-  let sqrt (x: f64) = intrinsics.sqrt64 x
-
-  let log (x: f64) = intrinsics.log64 x
-  let log2 (x: f64) = intrinsics.log2_64 x
-  let log10 (x: f64) = intrinsics.log10_64 x
-  let exp (x: f64) = intrinsics.exp64 x
-  let sin (x: f64) = intrinsics.sin64 x
-  let cos (x: f64) = intrinsics.cos64 x
-  let tan (x: f64) = intrinsics.tan64 x
-  let acos (x: f64) = intrinsics.acos64 x
-  let asin (x: f64) = intrinsics.asin64 x
-  let atan (x: f64) = intrinsics.atan64 x
-  let sinh (x: f64) = intrinsics.sinh64 x
-  let cosh (x: f64) = intrinsics.cosh64 x
-  let tanh (x: f64) = intrinsics.tanh64 x
-  let acosh (x: f64) = intrinsics.acosh64 x
-  let asinh (x: f64) = intrinsics.asinh64 x
-  let atanh (x: f64) = intrinsics.atanh64 x
-  let atan2 (x: f64) (y: f64) = intrinsics.atan2_64 (x, y)
-  let hypot (x: f64) (y: f64) = intrinsics.hypot64 (x, y)
-  let gamma = intrinsics.gamma64
-  let lgamma = intrinsics.lgamma64
-
-  let lerp v0 v1 t = intrinsics.lerp64 (v0,v1,t)
-  let fma a b c = intrinsics.fma64 (a,b,c)
-  let mad a b c = intrinsics.mad64 (a,b,c)
-
-  let ceil = intrinsics.ceil64
-  let floor = intrinsics.floor64
-  let trunc (x: f64) : f64 = i64 (i64m.f64 x)
-
-  let round = intrinsics.round64
-
-  let to_bits (x: f64): u64 = u64m.i64 (intrinsics.to_bits64 x)
-  let from_bits (x: u64): f64 = intrinsics.from_bits64 (intrinsics.sign_i64 x)
-
-  let num_bits = 64i32
-  let get_bit (bit: i32) (x: t) = u64m.get_bit bit (to_bits x)
-  let set_bit (bit: i32) (x: t) (b: i32) = from_bits (u64m.set_bit bit (to_bits x) b)
-
-  let isinf (x: f64) = intrinsics.isinf64 x
-  let isnan (x: f64) = intrinsics.isnan64 x
-
-  let inf = 1f64 / 0f64
-  let nan = 0f64 / 0f64
-
-  let highest = inf
-  let lowest = -inf
-  let epsilon = 2.220446049250313e-16f64
-
-  let pi = 3.1415926535897932384626433832795028841971693993751058209749445923078164062f64
-  let e = 2.718281828459045235360287471352662497757247093699959574966967627724076630353f64
-
-  let sum = reduce (+) (i32 0)
-  let product = reduce (*) (i32 1)
-  let maximum = reduce max lowest
-  let minimum = reduce min highest
-}
-
-module f32: (float with t = f32 with int_t = u32) = {
-  type t = f32
-  type int_t = u32
-
-  module i32m = i32
-  module u32m = u32
-  module f64m = f64
-
-  let (x: f32) + (y: f32) = intrinsics.fadd32 (x, y)
-  let (x: f32) - (y: f32) = intrinsics.fsub32 (x, y)
-  let (x: f32) * (y: f32) = intrinsics.fmul32 (x, y)
-  let (x: f32) / (y: f32) = intrinsics.fdiv32 (x, y)
-  let (x: f32) % (y: f32) = intrinsics.fmod32 (x, y)
-  let (x: f32) ** (y: f32) = intrinsics.fpow32 (x, y)
-
-  let u8  (x: u8)  = intrinsics.uitofp_i8_f32  (i8.u8 x)
-  let u16 (x: u16) = intrinsics.uitofp_i16_f32 (i16.u16 x)
-  let u32 (x: u32) = intrinsics.uitofp_i32_f32 (i32.u32 x)
-  let u64 (x: u64) = intrinsics.uitofp_i64_f32 (i64.u64 x)
-
-  let i8 (x: i8) = intrinsics.sitofp_i8_f32 x
-  let i16 (x: i16) = intrinsics.sitofp_i16_f32 x
-  let i32 (x: i32) = intrinsics.sitofp_i32_f32 x
-  let i64 (x: i64) = intrinsics.sitofp_i64_f32 x
-
-  let f16 (x: f16) = intrinsics.fpconv_f16_f32 x
-  let f32 (x: f32) = intrinsics.fpconv_f32_f32 x
-  let f64 (x: f64) = intrinsics.fpconv_f64_f32 x
-
-  let bool (x: bool) = if x then 1f32 else 0f32
-
-  let from_fraction (x: i64) (y: i64) = i64 x / i64 y
-  let to_i64 (x: f32) = intrinsics.fptosi_f32_i64 x
-  let to_f64 (x: f32) = intrinsics.fpconv_f32_f64 x
-
-  let (x: f32) == (y: f32) = intrinsics.eq_f32 (x, y)
-  let (x: f32) < (y: f32) = intrinsics.lt32 (x, y)
-  let (x: f32) > (y: f32) = intrinsics.lt32 (y, x)
-  let (x: f32) <= (y: f32) = intrinsics.le32 (x, y)
-  let (x: f32) >= (y: f32) = intrinsics.le32 (y, x)
-  let (x: f32) != (y: f32) = !(x == y)
-
-  let neg (x: t) = -x
-  let recip (x: t) = 1/x
-  let max (x: t) (y: t) = intrinsics.fmax32 (x, y)
-  let min (x: t) (y: t) = intrinsics.fmin32 (x, y)
-
-  let sgn (x: f32) = intrinsics.fsignum32 x
-  let abs (x: f32) = intrinsics.fabs32 x
-
-  let sqrt (x: f32) = intrinsics.sqrt32 x
-
-  let log (x: f32) = intrinsics.log32 x
-  let log2 (x: f32) = intrinsics.log2_32 x
-  let log10 (x: f32) = intrinsics.log10_32 x
-  let exp (x: f32) = intrinsics.exp32 x
-  let sin (x: f32) = intrinsics.sin32 x
-  let cos (x: f32) = intrinsics.cos32 x
-  let tan (x: f32) = intrinsics.tan32 x
-  let acos (x: f32) = intrinsics.acos32 x
-  let asin (x: f32) = intrinsics.asin32 x
-  let atan (x: f32) = intrinsics.atan32 x
-  let sinh (x: f32) = intrinsics.sinh32 x
-  let cosh (x: f32) = intrinsics.cosh32 x
-  let tanh (x: f32) = intrinsics.tanh32 x
-  let acosh (x: f32) = intrinsics.acosh32 x
-  let asinh (x: f32) = intrinsics.asinh32 x
-  let atanh (x: f32) = intrinsics.atanh32 x
-  let atan2 (x: f32) (y: f32) = intrinsics.atan2_32 (x, y)
-  let hypot (x: f32) (y: f32) = intrinsics.hypot32 (x, y)
-  let gamma = intrinsics.gamma32
-  let lgamma = intrinsics.lgamma32
-
-  let lerp v0 v1 t = intrinsics.lerp32 (v0,v1,t)
-  let fma a b c = intrinsics.fma32 (a,b,c)
-  let mad a b c = intrinsics.mad32 (a,b,c)
-
-  let ceil = intrinsics.ceil32
-  let floor = intrinsics.floor32
-  let trunc (x: f32) : f32 = i32 (i32m.f32 x)
-
-  let round = intrinsics.round32
-
-  let to_bits (x: f32): u32 = u32m.i32 (intrinsics.to_bits32 x)
-  let from_bits (x: u32): f32 = intrinsics.from_bits32 (intrinsics.sign_i32 x)
-
-  let num_bits = 32i32
-  let get_bit (bit: i32) (x: t) = u32m.get_bit bit (to_bits x)
-  let set_bit (bit: i32) (x: t) (b: i32) = from_bits (u32m.set_bit bit (to_bits x) b)
-
-  let isinf (x: f32) = intrinsics.isinf32 x
-  let isnan (x: f32) = intrinsics.isnan32 x
-
-  let inf = 1f32 / 0f32
-  let nan = 0f32 / 0f32
-
-  let highest = inf
-  let lowest = -inf
-  let epsilon = 1.1920929e-7f32
-
-  let pi = f64 f64m.pi
-  let e = f64 f64m.e
-
-  let sum = reduce (+) (i32 0)
-  let product = reduce (*) (i32 1)
-  let maximum = reduce max lowest
-  let minimum = reduce min highest
-}
-
--- | Emulated with single precision on systems that do not natively
--- support half precision.  This means you might get more accurate
--- results than on real systems, but it is also likely to be
--- significantly slower than just using `f32` in the first place.
-module f16: (float with t = f16 with int_t = u16) = {
-  type t = f16
-  type int_t = u16
-
-  module i16m = i16
-  module u16m = u16
-  module f64m = f64
-
-  let (x: f16) + (y: f16) = intrinsics.fadd16 (x, y)
-  let (x: f16) - (y: f16) = intrinsics.fsub16 (x, y)
-  let (x: f16) * (y: f16) = intrinsics.fmul16 (x, y)
-  let (x: f16) / (y: f16) = intrinsics.fdiv16 (x, y)
-  let (x: f16) % (y: f16) = intrinsics.fmod16 (x, y)
-  let (x: f16) ** (y: f16) = intrinsics.fpow16 (x, y)
-
-  let u8  (x: u8)  = intrinsics.uitofp_i8_f16  (i8.u8 x)
-  let u16 (x: u16) = intrinsics.uitofp_i16_f16 (i16.u16 x)
-  let u32 (x: u32) = intrinsics.uitofp_i32_f16 (i32.u32 x)
-  let u64 (x: u64) = intrinsics.uitofp_i64_f16 (i64.u64 x)
-
-  let i8 (x: i8) = intrinsics.sitofp_i8_f16 x
-  let i16 (x: i16) = intrinsics.sitofp_i16_f16 x
-  let i32 (x: i32) = intrinsics.sitofp_i32_f16 x
-  let i64 (x: i64) = intrinsics.sitofp_i64_f16 x
-
-  let f16 (x: f16) = intrinsics.fpconv_f16_f16 x
-  let f32 (x: f32) = intrinsics.fpconv_f32_f16 x
-  let f64 (x: f64) = intrinsics.fpconv_f64_f16 x
-
-  let bool (x: bool) = if x then 1f16 else 0f16
-
-  let from_fraction (x: i64) (y: i64) = i64 x / i64 y
-  let to_i64 (x: f16) = intrinsics.fptosi_f16_i64 x
-  let to_f64 (x: f16) = intrinsics.fpconv_f16_f64 x
-
-  let (x: f16) == (y: f16) = intrinsics.eq_f16 (x, y)
-  let (x: f16) < (y: f16) = intrinsics.lt16 (x, y)
-  let (x: f16) > (y: f16) = intrinsics.lt16 (y, x)
-  let (x: f16) <= (y: f16) = intrinsics.le16 (x, y)
-  let (x: f16) >= (y: f16) = intrinsics.le16 (y, x)
-  let (x: f16) != (y: f16) = !(x == y)
-
-  let neg (x: t) = -x
-  let recip (x: t) = 1/x
-  let max (x: t) (y: t) = intrinsics.fmax16 (x, y)
-  let min (x: t) (y: t) = intrinsics.fmin16 (x, y)
-
-  let sgn (x: f16) = intrinsics.fsignum16 x
-  let abs (x: f16) = intrinsics.fabs16 x
-
-  let sqrt (x: f16) = intrinsics.sqrt16 x
-
-  let log (x: f16) = intrinsics.log16 x
-  let log2 (x: f16) = intrinsics.log2_16 x
-  let log10 (x: f16) = intrinsics.log10_16 x
-  let exp (x: f16) = intrinsics.exp16 x
-  let sin (x: f16) = intrinsics.sin16 x
-  let cos (x: f16) = intrinsics.cos16 x
-  let tan (x: f16) = intrinsics.tan16 x
-  let acos (x: f16) = intrinsics.acos16 x
-  let asin (x: f16) = intrinsics.asin16 x
-  let atan (x: f16) = intrinsics.atan16 x
-  let sinh (x: f16) = intrinsics.sinh16 x
-  let cosh (x: f16) = intrinsics.cosh16 x
-  let tanh (x: f16) = intrinsics.tanh16 x
-  let acosh (x: f16) = intrinsics.acosh16 x
-  let asinh (x: f16) = intrinsics.asinh16 x
-  let atanh (x: f16) = intrinsics.atanh16 x
-  let atan2 (x: f16) (y: f16) = intrinsics.atan2_16 (x, y)
-  let hypot (x: f16) (y: f16) = intrinsics.hypot16 (x, y)
-  let gamma = intrinsics.gamma16
-  let lgamma = intrinsics.lgamma16
-
-  let lerp v0 v1 t = intrinsics.lerp16 (v0,v1,t)
-  let fma a b c = intrinsics.fma16 (a,b,c)
-  let mad a b c = intrinsics.mad16 (a,b,c)
-
-  let ceil = intrinsics.ceil16
-  let floor = intrinsics.floor16
-  let trunc (x: f16) : f16 = i16 (i16m.f16 x)
-
-  let round = intrinsics.round16
-
-  let to_bits (x: f16): u16 = u16m.i16 (intrinsics.to_bits16 x)
-  let from_bits (x: u16): f16 = intrinsics.from_bits16 (intrinsics.sign_i16 x)
-
-  let num_bits = 16i32
-  let get_bit (bit: i32) (x: t) = u16m.get_bit bit (to_bits x)
-  let set_bit (bit: i32) (x: t) (b: i32) = from_bits (u16m.set_bit bit (to_bits x) b)
-
-  let isinf (x: f16) = intrinsics.isinf16 x
-  let isnan (x: f16) = intrinsics.isnan16 x
-
-  let inf = 1f16 / 0f16
-  let nan = 0f16 / 0f16
-
-  let highest = inf
-  let lowest = -inf
-  let epsilon = 1.1920929e-7f16
-
-  let pi = f64 f64m.pi
-  let e = f64 f64m.e
-
-  let sum = reduce (+) (i32 0)
-  let product = reduce (*) (i32 1)
-  let maximum = reduce max lowest
-  let minimum = reduce min highest
+  def i8  = intrinsics.itob_i8_bool
+  def i16 = intrinsics.itob_i16_bool
+  def i32 = intrinsics.itob_i32_bool
+  def i64 = intrinsics.itob_i64_bool
+
+  def u8  (x: u8)  = intrinsics.itob_i8_bool (intrinsics.sign_i8 x)
+  def u16 (x: u16) = intrinsics.itob_i16_bool (intrinsics.sign_i16 x)
+  def u32 (x: u32) = intrinsics.itob_i32_bool (intrinsics.sign_i32 x)
+  def u64 (x: u64) = intrinsics.itob_i64_bool (intrinsics.sign_i64 x)
+
+  def f16 (x: f16) = x != 0f16
+  def f32 (x: f32) = x != 0f32
+  def f64 (x: f64) = x != 0f64
+
+  def bool (x: bool) = x
+}
+
+module i8: (integral with t = i8) = {
+  type t = i8
+
+  def (x: i8) + (y: i8) = intrinsics.add8 (x, y)
+  def (x: i8) - (y: i8) = intrinsics.sub8 (x, y)
+  def (x: i8) * (y: i8) = intrinsics.mul8 (x, y)
+  def (x: i8) / (y: i8) = intrinsics.sdiv8 (x, y)
+  def (x: i8) ** (y: i8) = intrinsics.pow8 (x, y)
+  def (x: i8) % (y: i8) = intrinsics.smod8 (x, y)
+  def (x: i8) // (y: i8) = intrinsics.squot8 (x, y)
+  def (x: i8) %% (y: i8) = intrinsics.srem8 (x, y)
+
+  def (x: i8) & (y: i8) = intrinsics.and8 (x, y)
+  def (x: i8) | (y: i8) = intrinsics.or8 (x, y)
+  def (x: i8) ^ (y: i8) = intrinsics.xor8 (x, y)
+  def not (x: i8) = intrinsics.complement8 x
+
+  def (x: i8) << (y: i8) = intrinsics.shl8 (x, y)
+  def (x: i8) >> (y: i8) = intrinsics.ashr8 (x, y)
+  def (x: i8) >>> (y: i8) = intrinsics.lshr8 (x, y)
+
+  def i8  (x: i8)  = intrinsics.sext_i8_i8 x
+  def i16 (x: i16) = intrinsics.sext_i16_i8 x
+  def i32 (x: i32) = intrinsics.sext_i32_i8 x
+  def i64 (x: i64) = intrinsics.sext_i64_i8 x
+
+  def u8  (x: u8)  = intrinsics.zext_i8_i8 (intrinsics.sign_i8 x)
+  def u16 (x: u16) = intrinsics.zext_i16_i8 (intrinsics.sign_i16 x)
+  def u32 (x: u32) = intrinsics.zext_i32_i8 (intrinsics.sign_i32 x)
+  def u64 (x: u64) = intrinsics.zext_i64_i8 (intrinsics.sign_i64 x)
+
+  def f16 (x: f16) = intrinsics.fptosi_f16_i8 x
+  def f32 (x: f32) = intrinsics.fptosi_f32_i8 x
+  def f64 (x: f64) = intrinsics.fptosi_f64_i8 x
+
+  def bool = intrinsics.btoi_bool_i8
+
+  def to_i32(x: i8) = intrinsics.sext_i8_i32 x
+  def to_i64(x: i8) = intrinsics.sext_i8_i64 x
+
+  def (x: i8) == (y: i8) = intrinsics.eq_i8 (x, y)
+  def (x: i8) < (y: i8) = intrinsics.slt8 (x, y)
+  def (x: i8) > (y: i8) = intrinsics.slt8 (y, x)
+  def (x: i8) <= (y: i8) = intrinsics.sle8 (x, y)
+  def (x: i8) >= (y: i8) = intrinsics.sle8 (y, x)
+  def (x: i8) != (y: i8) = !(x == y)
+
+  def sgn (x: i8) = intrinsics.ssignum8 x
+  def abs (x: i8) = intrinsics.abs8 x
+
+  def neg (x: t) = -x
+  def max (x: t) (y: t) = intrinsics.smax8 (x, y)
+  def min (x: t) (y: t) = intrinsics.smin8 (x, y)
+
+  def highest = 127i8
+  def lowest = highest + 1i8
+
+  def num_bits = 8i32
+  def get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
+  def set_bit (bit: i32) (x: t) (b: i32) =
+    ((x & i32 (!(1 intrinsics.<< bit))) | i32 (b intrinsics.<< bit))
+  def popc = intrinsics.popc8
+  def mul_hi a b = intrinsics.mul_hi8 (i8 a, i8 b)
+  def mad_hi a b c = intrinsics.mad_hi8 (i8 a, i8 b, i8 c)
+  def clz = intrinsics.clz8
+  def ctz = intrinsics.ctz8
+
+  def sum = reduce (+) (i32 0)
+  def product = reduce (*) (i32 1)
+  def maximum = reduce max lowest
+  def minimum = reduce min highest
+}
+
+module i16: (integral with t = i16) = {
+  type t = i16
+
+  def (x: i16) + (y: i16) = intrinsics.add16 (x, y)
+  def (x: i16) - (y: i16) = intrinsics.sub16 (x, y)
+  def (x: i16) * (y: i16) = intrinsics.mul16 (x, y)
+  def (x: i16) / (y: i16) = intrinsics.sdiv16 (x, y)
+  def (x: i16) ** (y: i16) = intrinsics.pow16 (x, y)
+  def (x: i16) % (y: i16) = intrinsics.smod16 (x, y)
+  def (x: i16) // (y: i16) = intrinsics.squot16 (x, y)
+  def (x: i16) %% (y: i16) = intrinsics.srem16 (x, y)
+
+  def (x: i16) & (y: i16) = intrinsics.and16 (x, y)
+  def (x: i16) | (y: i16) = intrinsics.or16 (x, y)
+  def (x: i16) ^ (y: i16) = intrinsics.xor16 (x, y)
+  def not (x: i16) = intrinsics.complement16 x
+
+  def (x: i16) << (y: i16) = intrinsics.shl16 (x, y)
+  def (x: i16) >> (y: i16) = intrinsics.ashr16 (x, y)
+  def (x: i16) >>> (y: i16) = intrinsics.lshr16 (x, y)
+
+  def i8  (x: i8)  = intrinsics.sext_i8_i16 x
+  def i16 (x: i16) = intrinsics.sext_i16_i16 x
+  def i32 (x: i32) = intrinsics.sext_i32_i16 x
+  def i64 (x: i64) = intrinsics.sext_i64_i16 x
+
+  def u8  (x: u8)  = intrinsics.zext_i8_i16 (intrinsics.sign_i8 x)
+  def u16 (x: u16) = intrinsics.zext_i16_i16 (intrinsics.sign_i16 x)
+  def u32 (x: u32) = intrinsics.zext_i32_i16 (intrinsics.sign_i32 x)
+  def u64 (x: u64) = intrinsics.zext_i64_i16 (intrinsics.sign_i64 x)
+
+  def f16 (x: f16) = intrinsics.fptosi_f16_i16 x
+  def f32 (x: f32) = intrinsics.fptosi_f32_i16 x
+  def f64 (x: f64) = intrinsics.fptosi_f64_i16 x
+
+  def bool = intrinsics.btoi_bool_i16
+
+  def to_i32(x: i16) = intrinsics.sext_i16_i32 x
+  def to_i64(x: i16) = intrinsics.sext_i16_i64 x
+
+  def (x: i16) == (y: i16) = intrinsics.eq_i16 (x, y)
+  def (x: i16) < (y: i16) = intrinsics.slt16 (x, y)
+  def (x: i16) > (y: i16) = intrinsics.slt16 (y, x)
+  def (x: i16) <= (y: i16) = intrinsics.sle16 (x, y)
+  def (x: i16) >= (y: i16) = intrinsics.sle16 (y, x)
+  def (x: i16) != (y: i16) = !(x == y)
+
+  def sgn (x: i16) = intrinsics.ssignum16 x
+  def abs (x: i16) = intrinsics.abs16 x
+
+  def neg (x: t) = -x
+  def max (x: t) (y: t) = intrinsics.smax16 (x, y)
+  def min (x: t) (y: t) = intrinsics.smin16 (x, y)
+
+  def highest = 32767i16
+  def lowest = highest + 1i16
+
+  def num_bits = 16i32
+  def get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
+  def set_bit (bit: i32) (x: t) (b: i32) =
+    ((x & i32 (!(1 intrinsics.<< bit))) | i32 (b intrinsics.<< bit))
+  def popc = intrinsics.popc16
+  def mul_hi a b = intrinsics.mul_hi16 (i16 a, i16 b)
+  def mad_hi a b c = intrinsics.mad_hi16 (i16 a, i16 b, i16 c)
+  def clz = intrinsics.clz16
+  def ctz = intrinsics.ctz16
+
+  def sum = reduce (+) (i32 0)
+  def product = reduce (*) (i32 1)
+  def maximum = reduce max lowest
+  def minimum = reduce min highest
+}
+
+module i32: (integral with t = i32) = {
+  type t = i32
+
+  def sign (x: u32) = intrinsics.sign_i32 x
+  def unsign (x: i32) = intrinsics.unsign_i32 x
+
+  def (x: i32) + (y: i32) = intrinsics.add32 (x, y)
+  def (x: i32) - (y: i32) = intrinsics.sub32 (x, y)
+  def (x: i32) * (y: i32) = intrinsics.mul32 (x, y)
+  def (x: i32) / (y: i32) = intrinsics.sdiv32 (x, y)
+  def (x: i32) ** (y: i32) = intrinsics.pow32 (x, y)
+  def (x: i32) % (y: i32) = intrinsics.smod32 (x, y)
+  def (x: i32) // (y: i32) = intrinsics.squot32 (x, y)
+  def (x: i32) %% (y: i32) = intrinsics.srem32 (x, y)
+
+  def (x: i32) & (y: i32) = intrinsics.and32 (x, y)
+  def (x: i32) | (y: i32) = intrinsics.or32 (x, y)
+  def (x: i32) ^ (y: i32) = intrinsics.xor32 (x, y)
+  def not (x: i32) = intrinsics.complement32 x
+
+  def (x: i32) << (y: i32) = intrinsics.shl32 (x, y)
+  def (x: i32) >> (y: i32) = intrinsics.ashr32 (x, y)
+  def (x: i32) >>> (y: i32) = intrinsics.lshr32 (x, y)
+
+  def i8  (x: i8)  = intrinsics.sext_i8_i32 x
+  def i16 (x: i16) = intrinsics.sext_i16_i32 x
+  def i32 (x: i32) = intrinsics.sext_i32_i32 x
+  def i64 (x: i64) = intrinsics.sext_i64_i32 x
+
+  def u8  (x: u8)  = intrinsics.zext_i8_i32 (intrinsics.sign_i8 x)
+  def u16 (x: u16) = intrinsics.zext_i16_i32 (intrinsics.sign_i16 x)
+  def u32 (x: u32) = intrinsics.zext_i32_i32 (intrinsics.sign_i32 x)
+  def u64 (x: u64) = intrinsics.zext_i64_i32 (intrinsics.sign_i64 x)
+
+  def f16 (x: f16) = intrinsics.fptosi_f16_i32 x
+  def f32 (x: f32) = intrinsics.fptosi_f32_i32 x
+  def f64 (x: f64) = intrinsics.fptosi_f64_i32 x
+
+  def bool = intrinsics.btoi_bool_i32
+
+  def to_i32(x: i32) = intrinsics.sext_i32_i32 x
+  def to_i64(x: i32) = intrinsics.sext_i32_i64 x
+
+  def (x: i32) == (y: i32) = intrinsics.eq_i32 (x, y)
+  def (x: i32) < (y: i32) = intrinsics.slt32 (x, y)
+  def (x: i32) > (y: i32) = intrinsics.slt32 (y, x)
+  def (x: i32) <= (y: i32) = intrinsics.sle32 (x, y)
+  def (x: i32) >= (y: i32) = intrinsics.sle32 (y, x)
+  def (x: i32) != (y: i32) = !(x == y)
+
+  def sgn (x: i32) = intrinsics.ssignum32 x
+  def abs (x: i32) = intrinsics.abs32 x
+
+  def neg (x: t) = -x
+  def max (x: t) (y: t) = intrinsics.smax32 (x, y)
+  def min (x: t) (y: t) = intrinsics.smin32 (x, y)
+
+  def highest = 2147483647i32
+  def lowest = highest + 1
+
+  def num_bits = 32i32
+  def get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
+  def set_bit (bit: i32) (x: t) (b: i32) =
+    ((x & i32 (!(1 intrinsics.<< bit))) | i32 (b intrinsics.<< bit))
+  def popc = intrinsics.popc32
+  def mul_hi a b = intrinsics.mul_hi32 (i32 a, i32 b)
+  def mad_hi a b c = intrinsics.mad_hi32 (i32 a, i32 b, i32 c)
+  def clz = intrinsics.clz32
+  def ctz = intrinsics.ctz32
+
+  def sum = reduce (+) (i32 0)
+  def product = reduce (*) (i32 1)
+  def maximum = reduce max lowest
+  def minimum = reduce min highest
+}
+
+module i64: (integral with t = i64) = {
+  type t = i64
+
+  def sign (x: u64) = intrinsics.sign_i64 x
+  def unsign (x: i64) = intrinsics.unsign_i64 x
+
+  def (x: i64) + (y: i64) = intrinsics.add64 (x, y)
+  def (x: i64) - (y: i64) = intrinsics.sub64 (x, y)
+  def (x: i64) * (y: i64) = intrinsics.mul64 (x, y)
+  def (x: i64) / (y: i64) = intrinsics.sdiv64 (x, y)
+  def (x: i64) ** (y: i64) = intrinsics.pow64 (x, y)
+  def (x: i64) % (y: i64) = intrinsics.smod64 (x, y)
+  def (x: i64) // (y: i64) = intrinsics.squot64 (x, y)
+  def (x: i64) %% (y: i64) = intrinsics.srem64 (x, y)
+
+  def (x: i64) & (y: i64) = intrinsics.and64 (x, y)
+  def (x: i64) | (y: i64) = intrinsics.or64 (x, y)
+  def (x: i64) ^ (y: i64) = intrinsics.xor64 (x, y)
+  def not (x: i64) = intrinsics.complement64 x
+
+  def (x: i64) << (y: i64) = intrinsics.shl64 (x, y)
+  def (x: i64) >> (y: i64) = intrinsics.ashr64 (x, y)
+  def (x: i64) >>> (y: i64) = intrinsics.lshr64 (x, y)
+
+  def i8  (x: i8)  = intrinsics.sext_i8_i64 x
+  def i16 (x: i16) = intrinsics.sext_i16_i64 x
+  def i32 (x: i32) = intrinsics.sext_i32_i64 x
+  def i64 (x: i64) = intrinsics.sext_i64_i64 x
+
+  def u8  (x: u8)  = intrinsics.zext_i8_i64 (intrinsics.sign_i8 x)
+  def u16 (x: u16) = intrinsics.zext_i16_i64 (intrinsics.sign_i16 x)
+  def u32 (x: u32) = intrinsics.zext_i32_i64 (intrinsics.sign_i32 x)
+  def u64 (x: u64) = intrinsics.zext_i64_i64 (intrinsics.sign_i64 x)
+
+  def f16 (x: f16) = intrinsics.fptosi_f16_i64 x
+  def f32 (x: f32) = intrinsics.fptosi_f32_i64 x
+  def f64 (x: f64) = intrinsics.fptosi_f64_i64 x
+
+  def bool = intrinsics.btoi_bool_i64
+
+  def to_i32(x: i64) = intrinsics.sext_i64_i32 x
+  def to_i64(x: i64) = intrinsics.sext_i64_i64 x
+
+  def (x: i64) == (y: i64) = intrinsics.eq_i64 (x, y)
+  def (x: i64) < (y: i64) = intrinsics.slt64 (x, y)
+  def (x: i64) > (y: i64) = intrinsics.slt64 (y, x)
+  def (x: i64) <= (y: i64) = intrinsics.sle64 (x, y)
+  def (x: i64) >= (y: i64) = intrinsics.sle64 (y, x)
+  def (x: i64) != (y: i64) = !(x == y)
+
+  def sgn (x: i64) = intrinsics.ssignum64 x
+  def abs (x: i64) = intrinsics.abs64 x
+
+  def neg (x: t) = -x
+  def max (x: t) (y: t) = intrinsics.smax64 (x, y)
+  def min (x: t) (y: t) = intrinsics.smin64 (x, y)
+
+  def highest = 9223372036854775807i64
+  def lowest = highest + 1i64
+
+  def num_bits = 64i32
+  def get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
+  def set_bit (bit: i32) (x: t) (b: i32) =
+    ((x & i32 (!(1 intrinsics.<< bit))) | intrinsics.zext_i32_i64 (b intrinsics.<< bit))
+  def popc = intrinsics.popc64
+  def mul_hi a b = intrinsics.mul_hi64 (i64 a, i64 b)
+  def mad_hi a b c = intrinsics.mad_hi64 (i64 a, i64 b, i64 c)
+  def clz = intrinsics.clz64
+  def ctz = intrinsics.ctz64
+
+  def sum = reduce (+) (i32 0)
+  def product = reduce (*) (i32 1)
+  def maximum = reduce max lowest
+  def minimum = reduce min highest
+}
+
+module u8: (integral with t = u8) = {
+  type t = u8
+
+  def sign (x: u8) = intrinsics.sign_i8 x
+  def unsign (x: i8) = intrinsics.unsign_i8 x
+
+  def (x: u8) + (y: u8) = unsign (intrinsics.add8 (sign x, sign y))
+  def (x: u8) - (y: u8) = unsign (intrinsics.sub8 (sign x, sign y))
+  def (x: u8) * (y: u8) = unsign (intrinsics.mul8 (sign x, sign y))
+  def (x: u8) / (y: u8) = unsign (intrinsics.udiv8 (sign x, sign y))
+  def (x: u8) ** (y: u8) = unsign (intrinsics.pow8 (sign x, sign y))
+  def (x: u8) % (y: u8) = unsign (intrinsics.umod8 (sign x, sign y))
+  def (x: u8) // (y: u8) = unsign (intrinsics.udiv8 (sign x, sign y))
+  def (x: u8) %% (y: u8) = unsign (intrinsics.umod8 (sign x, sign y))
+
+  def (x: u8) & (y: u8) = unsign (intrinsics.and8 (sign x, sign y))
+  def (x: u8) | (y: u8) = unsign (intrinsics.or8 (sign x, sign y))
+  def (x: u8) ^ (y: u8) = unsign (intrinsics.xor8 (sign x, sign y))
+  def not (x: u8) = unsign (intrinsics.complement8 (sign x))
+
+  def (x: u8) << (y: u8) = unsign (intrinsics.shl8 (sign x, sign y))
+  def (x: u8) >> (y: u8) = unsign (intrinsics.ashr8 (sign x, sign y))
+  def (x: u8) >>> (y: u8) = unsign (intrinsics.lshr8 (sign x, sign y))
+
+  def u8  (x: u8)  = unsign (i8.u8 x)
+  def u16 (x: u16) = unsign (i8.u16 x)
+  def u32 (x: u32) = unsign (i8.u32 x)
+  def u64 (x: u64) = unsign (i8.u64 x)
+
+  def i8  (x: i8)  = unsign (intrinsics.zext_i8_i8 x)
+  def i16 (x: i16) = unsign (intrinsics.zext_i16_i8 x)
+  def i32 (x: i32) = unsign (intrinsics.zext_i32_i8 x)
+  def i64 (x: i64) = unsign (intrinsics.zext_i64_i8 x)
+
+  def f16 (x: f16) = unsign (intrinsics.fptoui_f16_i8 x)
+  def f32 (x: f32) = unsign (intrinsics.fptoui_f32_i8 x)
+  def f64 (x: f64) = unsign (intrinsics.fptoui_f64_i8 x)
+
+  def bool x = unsign (intrinsics.btoi_bool_i8 x)
+
+  def to_i32(x: u8) = intrinsics.zext_i8_i32 (sign x)
+  def to_i64(x: u8) = intrinsics.zext_i8_i64 (sign x)
+
+  def (x: u8) == (y: u8) = intrinsics.eq_i8 (sign x, sign y)
+  def (x: u8) < (y: u8) = intrinsics.ult8 (sign x, sign y)
+  def (x: u8) > (y: u8) = intrinsics.ult8 (sign y, sign x)
+  def (x: u8) <= (y: u8) = intrinsics.ule8 (sign x, sign y)
+  def (x: u8) >= (y: u8) = intrinsics.ule8 (sign y, sign x)
+  def (x: u8) != (y: u8) = !(x == y)
+
+  def sgn (x: u8) = unsign (intrinsics.usignum8 (sign x))
+  def abs (x: u8) = x
+
+  def neg (x: t) = -x
+  def max (x: t) (y: t) = unsign (intrinsics.umax8 (sign x, sign y))
+  def min (x: t) (y: t) = unsign (intrinsics.umin8 (sign x, sign y))
+
+  def highest = 255u8
+  def lowest = 0u8
+
+  def num_bits = 8i32
+  def get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
+  def set_bit (bit: i32) (x: t) (b: i32) =
+    ((x & i32 (!(1 intrinsics.<< bit))) | i32 (b intrinsics.<< bit))
+  def popc x = intrinsics.popc8 (sign x)
+  def mul_hi a b = unsign (intrinsics.mul_hi8 (sign a, sign b))
+  def mad_hi a b c = unsign (intrinsics.mad_hi8 (sign a, sign b, sign c))
+  def clz x = intrinsics.clz8 (sign x)
+  def ctz x = intrinsics.ctz8 (sign x)
+
+  def sum = reduce (+) (i32 0)
+  def product = reduce (*) (i32 1)
+  def maximum = reduce max lowest
+  def minimum = reduce min highest
+}
+
+module u16: (integral with t = u16) = {
+  type t = u16
+
+  def sign (x: u16) = intrinsics.sign_i16 x
+  def unsign (x: i16) = intrinsics.unsign_i16 x
+
+  def (x: u16) + (y: u16) = unsign (intrinsics.add16 (sign x, sign y))
+  def (x: u16) - (y: u16) = unsign (intrinsics.sub16 (sign x, sign y))
+  def (x: u16) * (y: u16) = unsign (intrinsics.mul16 (sign x, sign y))
+  def (x: u16) / (y: u16) = unsign (intrinsics.udiv16 (sign x, sign y))
+  def (x: u16) ** (y: u16) = unsign (intrinsics.pow16 (sign x, sign y))
+  def (x: u16) % (y: u16) = unsign (intrinsics.umod16 (sign x, sign y))
+  def (x: u16) // (y: u16) = unsign (intrinsics.udiv16 (sign x, sign y))
+  def (x: u16) %% (y: u16) = unsign (intrinsics.umod16 (sign x, sign y))
+
+  def (x: u16) & (y: u16) = unsign (intrinsics.and16 (sign x, sign y))
+  def (x: u16) | (y: u16) = unsign (intrinsics.or16 (sign x, sign y))
+  def (x: u16) ^ (y: u16) = unsign (intrinsics.xor16 (sign x, sign y))
+  def not (x: u16) = unsign (intrinsics.complement16 (sign x))
+
+  def (x: u16) << (y: u16) = unsign (intrinsics.shl16 (sign x, sign y))
+  def (x: u16) >> (y: u16) = unsign (intrinsics.ashr16 (sign x, sign y))
+  def (x: u16) >>> (y: u16) = unsign (intrinsics.lshr16 (sign x, sign y))
+
+  def u8  (x: u8)  = unsign (i16.u8 x)
+  def u16 (x: u16) = unsign (i16.u16 x)
+  def u32 (x: u32) = unsign (i16.u32 x)
+  def u64 (x: u64) = unsign (i16.u64 x)
+
+  def i8  (x: i8)  = unsign (intrinsics.zext_i8_i16 x)
+  def i16 (x: i16) = unsign (intrinsics.zext_i16_i16 x)
+  def i32 (x: i32) = unsign (intrinsics.zext_i32_i16 x)
+  def i64 (x: i64) = unsign (intrinsics.zext_i64_i16 x)
+
+  def f16 (x: f16) = unsign (intrinsics.fptoui_f16_i16 x)
+  def f32 (x: f32) = unsign (intrinsics.fptoui_f32_i16 x)
+  def f64 (x: f64) = unsign (intrinsics.fptoui_f64_i16 x)
+
+  def bool x = unsign (intrinsics.btoi_bool_i16 x)
+
+  def to_i32(x: u16) = intrinsics.zext_i16_i32 (sign x)
+  def to_i64(x: u16) = intrinsics.zext_i16_i64 (sign x)
+
+  def (x: u16) == (y: u16) = intrinsics.eq_i16 (sign x, sign y)
+  def (x: u16) < (y: u16) = intrinsics.ult16 (sign x, sign y)
+  def (x: u16) > (y: u16) = intrinsics.ult16 (sign y, sign x)
+  def (x: u16) <= (y: u16) = intrinsics.ule16 (sign x, sign y)
+  def (x: u16) >= (y: u16) = intrinsics.ule16 (sign y, sign x)
+  def (x: u16) != (y: u16) = !(x == y)
+
+  def sgn (x: u16) = unsign (intrinsics.usignum16 (sign x))
+  def abs (x: u16) = x
+
+  def neg (x: t) = -x
+  def max (x: t) (y: t) = unsign (intrinsics.umax16 (sign x, sign y))
+  def min (x: t) (y: t) = unsign (intrinsics.umin16 (sign x, sign y))
+
+  def highest = 65535u16
+  def lowest = 0u16
+
+  def num_bits = 16i32
+  def get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
+  def set_bit (bit: i32) (x: t) (b: i32) =
+    ((x & i32 (!(1 intrinsics.<< bit))) | i32 (b intrinsics.<< bit))
+  def popc x = intrinsics.popc16 (sign x)
+  def mul_hi a b = unsign (intrinsics.mul_hi16 (sign a, sign b))
+  def mad_hi a b c = unsign (intrinsics.mad_hi16 (sign a, sign b, sign c))
+  def clz x = intrinsics.clz16 (sign x)
+  def ctz x = intrinsics.ctz16 (sign x)
+
+  def sum = reduce (+) (i32 0)
+  def product = reduce (*) (i32 1)
+  def maximum = reduce max lowest
+  def minimum = reduce min highest
+}
+
+module u32: (integral with t = u32) = {
+  type t = u32
+
+  def sign (x: u32) = intrinsics.sign_i32 x
+  def unsign (x: i32) = intrinsics.unsign_i32 x
+
+  def (x: u32) + (y: u32) = unsign (intrinsics.add32 (sign x, sign y))
+  def (x: u32) - (y: u32) = unsign (intrinsics.sub32 (sign x, sign y))
+  def (x: u32) * (y: u32) = unsign (intrinsics.mul32 (sign x, sign y))
+  def (x: u32) / (y: u32) = unsign (intrinsics.udiv32 (sign x, sign y))
+  def (x: u32) ** (y: u32) = unsign (intrinsics.pow32 (sign x, sign y))
+  def (x: u32) % (y: u32) = unsign (intrinsics.umod32 (sign x, sign y))
+  def (x: u32) // (y: u32) = unsign (intrinsics.udiv32 (sign x, sign y))
+  def (x: u32) %% (y: u32) = unsign (intrinsics.umod32 (sign x, sign y))
+
+  def (x: u32) & (y: u32) = unsign (intrinsics.and32 (sign x, sign y))
+  def (x: u32) | (y: u32) = unsign (intrinsics.or32 (sign x, sign y))
+  def (x: u32) ^ (y: u32) = unsign (intrinsics.xor32 (sign x, sign y))
+  def not (x: u32) = unsign (intrinsics.complement32 (sign x))
+
+  def (x: u32) << (y: u32) = unsign (intrinsics.shl32 (sign x, sign y))
+  def (x: u32) >> (y: u32) = unsign (intrinsics.ashr32 (sign x, sign y))
+  def (x: u32) >>> (y: u32) = unsign (intrinsics.lshr32 (sign x, sign y))
+
+  def u8  (x: u8)  = unsign (i32.u8 x)
+  def u16 (x: u16) = unsign (i32.u16 x)
+  def u32 (x: u32) = unsign (i32.u32 x)
+  def u64 (x: u64) = unsign (i32.u64 x)
+
+  def i8  (x: i8)  = unsign (intrinsics.zext_i8_i32 x)
+  def i16 (x: i16) = unsign (intrinsics.zext_i16_i32 x)
+  def i32 (x: i32) = unsign (intrinsics.zext_i32_i32 x)
+  def i64 (x: i64) = unsign (intrinsics.zext_i64_i32 x)
+
+  def f16 (x: f16) = unsign (intrinsics.fptoui_f16_i32 x)
+  def f32 (x: f32) = unsign (intrinsics.fptoui_f32_i32 x)
+  def f64 (x: f64) = unsign (intrinsics.fptoui_f64_i32 x)
+
+  def bool x = unsign (intrinsics.btoi_bool_i32 x)
+
+  def to_i32(x: u32) = intrinsics.zext_i32_i32 (sign x)
+  def to_i64(x: u32) = intrinsics.zext_i32_i64 (sign x)
+
+  def (x: u32) == (y: u32) = intrinsics.eq_i32 (sign x, sign y)
+  def (x: u32) < (y: u32) = intrinsics.ult32 (sign x, sign y)
+  def (x: u32) > (y: u32) = intrinsics.ult32 (sign y, sign x)
+  def (x: u32) <= (y: u32) = intrinsics.ule32 (sign x, sign y)
+  def (x: u32) >= (y: u32) = intrinsics.ule32 (sign y, sign x)
+  def (x: u32) != (y: u32) = !(x == y)
+
+  def sgn (x: u32) = unsign (intrinsics.usignum32 (sign x))
+  def abs (x: u32) = x
+
+  def highest = 4294967295u32
+  def lowest = highest + 1u32
+
+  def neg (x: t) = -x
+  def max (x: t) (y: t) = unsign (intrinsics.umax32 (sign x, sign y))
+  def min (x: t) (y: t) = unsign (intrinsics.umin32 (sign x, sign y))
+
+  def num_bits = 32i32
+  def get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
+  def set_bit (bit: i32) (x: t) (b: i32) =
+    ((x & i32 (!(1 intrinsics.<< bit))) | i32 (b intrinsics.<< bit))
+  def popc x = intrinsics.popc32 (sign x)
+  def mul_hi a b = unsign (intrinsics.mul_hi32 (sign a, sign b))
+  def mad_hi a b c = unsign (intrinsics.mad_hi32 (sign a, sign b, sign c))
+  def clz x = intrinsics.clz32 (sign x)
+  def ctz x = intrinsics.ctz32 (sign x)
+
+  def sum = reduce (+) (i32 0)
+  def product = reduce (*) (i32 1)
+  def maximum = reduce max lowest
+  def minimum = reduce min highest
+}
+
+module u64: (integral with t = u64) = {
+  type t = u64
+
+  def sign (x: u64) = intrinsics.sign_i64 x
+  def unsign (x: i64) = intrinsics.unsign_i64 x
+
+  def (x: u64) + (y: u64) = unsign (intrinsics.add64 (sign x, sign y))
+  def (x: u64) - (y: u64) = unsign (intrinsics.sub64 (sign x, sign y))
+  def (x: u64) * (y: u64) = unsign (intrinsics.mul64 (sign x, sign y))
+  def (x: u64) / (y: u64) = unsign (intrinsics.udiv64 (sign x, sign y))
+  def (x: u64) ** (y: u64) = unsign (intrinsics.pow64 (sign x, sign y))
+  def (x: u64) % (y: u64) = unsign (intrinsics.umod64 (sign x, sign y))
+  def (x: u64) // (y: u64) = unsign (intrinsics.udiv64 (sign x, sign y))
+  def (x: u64) %% (y: u64) = unsign (intrinsics.umod64 (sign x, sign y))
+
+  def (x: u64) & (y: u64) = unsign (intrinsics.and64 (sign x, sign y))
+  def (x: u64) | (y: u64) = unsign (intrinsics.or64 (sign x, sign y))
+  def (x: u64) ^ (y: u64) = unsign (intrinsics.xor64 (sign x, sign y))
+  def not (x: u64) = unsign (intrinsics.complement64 (sign x))
+
+  def (x: u64) << (y: u64) = unsign (intrinsics.shl64 (sign x, sign y))
+  def (x: u64) >> (y: u64) = unsign (intrinsics.ashr64 (sign x, sign y))
+  def (x: u64) >>> (y: u64) = unsign (intrinsics.lshr64 (sign x, sign y))
+
+  def u8  (x: u8)  = unsign (i64.u8 x)
+  def u16 (x: u16) = unsign (i64.u16 x)
+  def u32 (x: u32) = unsign (i64.u32 x)
+  def u64 (x: u64) = unsign (i64.u64 x)
+
+  def i8 (x: i8)   = unsign (intrinsics.zext_i8_i64 x)
+  def i16 (x: i16) = unsign (intrinsics.zext_i16_i64 x)
+  def i32 (x: i32) = unsign (intrinsics.zext_i32_i64 x)
+  def i64 (x: i64) = unsign (intrinsics.zext_i64_i64 x)
+
+  def f16 (x: f16) = unsign (intrinsics.fptoui_f16_i64 x)
+  def f32 (x: f32) = unsign (intrinsics.fptoui_f32_i64 x)
+  def f64 (x: f64) = unsign (intrinsics.fptoui_f64_i64 x)
+
+  def bool x = unsign (intrinsics.btoi_bool_i64 x)
+
+  def to_i32(x: u64) = intrinsics.zext_i64_i32 (sign x)
+  def to_i64(x: u64) = intrinsics.zext_i64_i64 (sign x)
+
+  def (x: u64) == (y: u64) = intrinsics.eq_i64 (sign x, sign y)
+  def (x: u64) < (y: u64) = intrinsics.ult64 (sign x, sign y)
+  def (x: u64) > (y: u64) = intrinsics.ult64 (sign y, sign x)
+  def (x: u64) <= (y: u64) = intrinsics.ule64 (sign x, sign y)
+  def (x: u64) >= (y: u64) = intrinsics.ule64 (sign y, sign x)
+  def (x: u64) != (y: u64) = !(x == y)
+
+  def sgn (x: u64) = unsign (intrinsics.usignum64 (sign x))
+  def abs (x: u64) = x
+
+  def neg (x: t) = -x
+  def max (x: t) (y: t) = unsign (intrinsics.umax64 (sign x, sign y))
+  def min (x: t) (y: t) = unsign (intrinsics.umin64 (sign x, sign y))
+
+  def highest = 18446744073709551615u64
+  def lowest = highest + 1u64
+
+  def num_bits = 64i32
+  def get_bit (bit: i32) (x: t) = to_i32 ((x >> i32 bit) & i32 1)
+  def set_bit (bit: i32) (x: t) (b: i32) =
+    ((x & i32 (!(1 intrinsics.<< bit))) | i32 (b intrinsics.<< bit))
+  def popc x = intrinsics.popc64 (sign x)
+  def mul_hi a b = unsign (intrinsics.mul_hi64 (sign a, sign b))
+  def mad_hi a b c = unsign (intrinsics.mad_hi64 (sign a, sign b, sign c))
+  def clz x = intrinsics.clz64 (sign x)
+  def ctz x = intrinsics.ctz64 (sign x)
+
+  def sum = reduce (+) (i32 0)
+  def product = reduce (*) (i32 1)
+  def maximum = reduce max lowest
+  def minimum = reduce min highest
+}
+
+module f64: (float with t = f64 with int_t = u64) = {
+  type t = f64
+  type int_t = u64
+
+  module i64m = i64
+  module u64m = u64
+
+  def (x: f64) + (y: f64) = intrinsics.fadd64 (x, y)
+  def (x: f64) - (y: f64) = intrinsics.fsub64 (x, y)
+  def (x: f64) * (y: f64) = intrinsics.fmul64 (x, y)
+  def (x: f64) / (y: f64) = intrinsics.fdiv64 (x, y)
+  def (x: f64) % (y: f64) = intrinsics.fmod64 (x, y)
+  def (x: f64) ** (y: f64) = intrinsics.fpow64 (x, y)
+
+  def u8  (x: u8)  = intrinsics.uitofp_i8_f64  (i8.u8 x)
+  def u16 (x: u16) = intrinsics.uitofp_i16_f64 (i16.u16 x)
+  def u32 (x: u32) = intrinsics.uitofp_i32_f64 (i32.u32 x)
+  def u64 (x: u64) = intrinsics.uitofp_i64_f64 (i64.u64 x)
+
+  def i8 (x: i8) = intrinsics.sitofp_i8_f64 x
+  def i16 (x: i16) = intrinsics.sitofp_i16_f64 x
+  def i32 (x: i32) = intrinsics.sitofp_i32_f64 x
+  def i64 (x: i64) = intrinsics.sitofp_i64_f64 x
+
+  def f16 (x: f16) = intrinsics.fpconv_f16_f64 x
+  def f32 (x: f32) = intrinsics.fpconv_f32_f64 x
+  def f64 (x: f64) = intrinsics.fpconv_f64_f64 x
+
+  def bool (x: bool) = if x then 1f64 else 0f64
+
+  def from_fraction (x: i64) (y: i64) = i64 x / i64 y
+  def to_i64 (x: f64) = intrinsics.fptosi_f64_i64 x
+  def to_f64 (x: f64) = x
+
+  def (x: f64) == (y: f64) = intrinsics.eq_f64 (x, y)
+  def (x: f64) < (y: f64) = intrinsics.lt64 (x, y)
+  def (x: f64) > (y: f64) = intrinsics.lt64 (y, x)
+  def (x: f64) <= (y: f64) = intrinsics.le64 (x, y)
+  def (x: f64) >= (y: f64) = intrinsics.le64 (y, x)
+  def (x: f64) != (y: f64) = !(x == y)
+
+  def neg (x: t) = -x
+  def recip (x: t) = 1/x
+  def max (x: t) (y: t) = intrinsics.fmax64 (x, y)
+  def min (x: t) (y: t) = intrinsics.fmin64 (x, y)
+
+  def sgn (x: f64) = intrinsics.fsignum64 x
+  def abs (x: f64) = intrinsics.fabs64 x
+
+  def sqrt (x: f64) = intrinsics.sqrt64 x
+
+  def log (x: f64) = intrinsics.log64 x
+  def log2 (x: f64) = intrinsics.log2_64 x
+  def log10 (x: f64) = intrinsics.log10_64 x
+  def exp (x: f64) = intrinsics.exp64 x
+  def sin (x: f64) = intrinsics.sin64 x
+  def cos (x: f64) = intrinsics.cos64 x
+  def tan (x: f64) = intrinsics.tan64 x
+  def acos (x: f64) = intrinsics.acos64 x
+  def asin (x: f64) = intrinsics.asin64 x
+  def atan (x: f64) = intrinsics.atan64 x
+  def sinh (x: f64) = intrinsics.sinh64 x
+  def cosh (x: f64) = intrinsics.cosh64 x
+  def tanh (x: f64) = intrinsics.tanh64 x
+  def acosh (x: f64) = intrinsics.acosh64 x
+  def asinh (x: f64) = intrinsics.asinh64 x
+  def atanh (x: f64) = intrinsics.atanh64 x
+  def atan2 (x: f64) (y: f64) = intrinsics.atan2_64 (x, y)
+  def hypot (x: f64) (y: f64) = intrinsics.hypot64 (x, y)
+  def gamma = intrinsics.gamma64
+  def lgamma = intrinsics.lgamma64
+
+  def lerp v0 v1 t = intrinsics.lerp64 (v0,v1,t)
+  def fma a b c = intrinsics.fma64 (a,b,c)
+  def mad a b c = intrinsics.mad64 (a,b,c)
+
+  def ceil = intrinsics.ceil64
+  def floor = intrinsics.floor64
+  def trunc (x: f64) : f64 = i64 (i64m.f64 x)
+
+  def round = intrinsics.round64
+
+  def to_bits (x: f64): u64 = u64m.i64 (intrinsics.to_bits64 x)
+  def from_bits (x: u64): f64 = intrinsics.from_bits64 (intrinsics.sign_i64 x)
+
+  def num_bits = 64i32
+  def get_bit (bit: i32) (x: t) = u64m.get_bit bit (to_bits x)
+  def set_bit (bit: i32) (x: t) (b: i32) = from_bits (u64m.set_bit bit (to_bits x) b)
+
+  def isinf (x: f64) = intrinsics.isinf64 x
+  def isnan (x: f64) = intrinsics.isnan64 x
+
+  def inf = 1f64 / 0f64
+  def nan = 0f64 / 0f64
+
+  def highest = inf
+  def lowest = -inf
+  def epsilon = 2.220446049250313e-16f64
+
+  def pi = 3.1415926535897932384626433832795028841971693993751058209749445923078164062f64
+  def e = 2.718281828459045235360287471352662497757247093699959574966967627724076630353f64
+
+  def sum = reduce (+) (i32 0)
+  def product = reduce (*) (i32 1)
+  def maximum = reduce max lowest
+  def minimum = reduce min highest
+}
+
+module f32: (float with t = f32 with int_t = u32) = {
+  type t = f32
+  type int_t = u32
+
+  module i32m = i32
+  module u32m = u32
+  module f64m = f64
+
+  def (x: f32) + (y: f32) = intrinsics.fadd32 (x, y)
+  def (x: f32) - (y: f32) = intrinsics.fsub32 (x, y)
+  def (x: f32) * (y: f32) = intrinsics.fmul32 (x, y)
+  def (x: f32) / (y: f32) = intrinsics.fdiv32 (x, y)
+  def (x: f32) % (y: f32) = intrinsics.fmod32 (x, y)
+  def (x: f32) ** (y: f32) = intrinsics.fpow32 (x, y)
+
+  def u8  (x: u8)  = intrinsics.uitofp_i8_f32  (i8.u8 x)
+  def u16 (x: u16) = intrinsics.uitofp_i16_f32 (i16.u16 x)
+  def u32 (x: u32) = intrinsics.uitofp_i32_f32 (i32.u32 x)
+  def u64 (x: u64) = intrinsics.uitofp_i64_f32 (i64.u64 x)
+
+  def i8 (x: i8) = intrinsics.sitofp_i8_f32 x
+  def i16 (x: i16) = intrinsics.sitofp_i16_f32 x
+  def i32 (x: i32) = intrinsics.sitofp_i32_f32 x
+  def i64 (x: i64) = intrinsics.sitofp_i64_f32 x
+
+  def f16 (x: f16) = intrinsics.fpconv_f16_f32 x
+  def f32 (x: f32) = intrinsics.fpconv_f32_f32 x
+  def f64 (x: f64) = intrinsics.fpconv_f64_f32 x
+
+  def bool (x: bool) = if x then 1f32 else 0f32
+
+  def from_fraction (x: i64) (y: i64) = i64 x / i64 y
+  def to_i64 (x: f32) = intrinsics.fptosi_f32_i64 x
+  def to_f64 (x: f32) = intrinsics.fpconv_f32_f64 x
+
+  def (x: f32) == (y: f32) = intrinsics.eq_f32 (x, y)
+  def (x: f32) < (y: f32) = intrinsics.lt32 (x, y)
+  def (x: f32) > (y: f32) = intrinsics.lt32 (y, x)
+  def (x: f32) <= (y: f32) = intrinsics.le32 (x, y)
+  def (x: f32) >= (y: f32) = intrinsics.le32 (y, x)
+  def (x: f32) != (y: f32) = !(x == y)
+
+  def neg (x: t) = -x
+  def recip (x: t) = 1/x
+  def max (x: t) (y: t) = intrinsics.fmax32 (x, y)
+  def min (x: t) (y: t) = intrinsics.fmin32 (x, y)
+
+  def sgn (x: f32) = intrinsics.fsignum32 x
+  def abs (x: f32) = intrinsics.fabs32 x
+
+  def sqrt (x: f32) = intrinsics.sqrt32 x
+
+  def log (x: f32) = intrinsics.log32 x
+  def log2 (x: f32) = intrinsics.log2_32 x
+  def log10 (x: f32) = intrinsics.log10_32 x
+  def exp (x: f32) = intrinsics.exp32 x
+  def sin (x: f32) = intrinsics.sin32 x
+  def cos (x: f32) = intrinsics.cos32 x
+  def tan (x: f32) = intrinsics.tan32 x
+  def acos (x: f32) = intrinsics.acos32 x
+  def asin (x: f32) = intrinsics.asin32 x
+  def atan (x: f32) = intrinsics.atan32 x
+  def sinh (x: f32) = intrinsics.sinh32 x
+  def cosh (x: f32) = intrinsics.cosh32 x
+  def tanh (x: f32) = intrinsics.tanh32 x
+  def acosh (x: f32) = intrinsics.acosh32 x
+  def asinh (x: f32) = intrinsics.asinh32 x
+  def atanh (x: f32) = intrinsics.atanh32 x
+  def atan2 (x: f32) (y: f32) = intrinsics.atan2_32 (x, y)
+  def hypot (x: f32) (y: f32) = intrinsics.hypot32 (x, y)
+  def gamma = intrinsics.gamma32
+  def lgamma = intrinsics.lgamma32
+
+  def lerp v0 v1 t = intrinsics.lerp32 (v0,v1,t)
+  def fma a b c = intrinsics.fma32 (a,b,c)
+  def mad a b c = intrinsics.mad32 (a,b,c)
+
+  def ceil = intrinsics.ceil32
+  def floor = intrinsics.floor32
+  def trunc (x: f32) : f32 = i32 (i32m.f32 x)
+
+  def round = intrinsics.round32
+
+  def to_bits (x: f32): u32 = u32m.i32 (intrinsics.to_bits32 x)
+  def from_bits (x: u32): f32 = intrinsics.from_bits32 (intrinsics.sign_i32 x)
+
+  def num_bits = 32i32
+  def get_bit (bit: i32) (x: t) = u32m.get_bit bit (to_bits x)
+  def set_bit (bit: i32) (x: t) (b: i32) = from_bits (u32m.set_bit bit (to_bits x) b)
+
+  def isinf (x: f32) = intrinsics.isinf32 x
+  def isnan (x: f32) = intrinsics.isnan32 x
+
+  def inf = 1f32 / 0f32
+  def nan = 0f32 / 0f32
+
+  def highest = inf
+  def lowest = -inf
+  def epsilon = 1.1920929e-7f32
+
+  def pi = f64 f64m.pi
+  def e = f64 f64m.e
+
+  def sum = reduce (+) (i32 0)
+  def product = reduce (*) (i32 1)
+  def maximum = reduce max lowest
+  def minimum = reduce min highest
+}
+
+-- | Emulated with single precision on systems that do not natively
+-- support half precision.  This means you might get more accurate
+-- results than on real systems, but it is also likely to be
+-- significantly slower than just using `f32` in the first place.
+module f16: (float with t = f16 with int_t = u16) = {
+  type t = f16
+  type int_t = u16
+
+  module i16m = i16
+  module u16m = u16
+  module f64m = f64
+
+  def (x: f16) + (y: f16) = intrinsics.fadd16 (x, y)
+  def (x: f16) - (y: f16) = intrinsics.fsub16 (x, y)
+  def (x: f16) * (y: f16) = intrinsics.fmul16 (x, y)
+  def (x: f16) / (y: f16) = intrinsics.fdiv16 (x, y)
+  def (x: f16) % (y: f16) = intrinsics.fmod16 (x, y)
+  def (x: f16) ** (y: f16) = intrinsics.fpow16 (x, y)
+
+  def u8  (x: u8)  = intrinsics.uitofp_i8_f16  (i8.u8 x)
+  def u16 (x: u16) = intrinsics.uitofp_i16_f16 (i16.u16 x)
+  def u32 (x: u32) = intrinsics.uitofp_i32_f16 (i32.u32 x)
+  def u64 (x: u64) = intrinsics.uitofp_i64_f16 (i64.u64 x)
+
+  def i8 (x: i8) = intrinsics.sitofp_i8_f16 x
+  def i16 (x: i16) = intrinsics.sitofp_i16_f16 x
+  def i32 (x: i32) = intrinsics.sitofp_i32_f16 x
+  def i64 (x: i64) = intrinsics.sitofp_i64_f16 x
+
+  def f16 (x: f16) = intrinsics.fpconv_f16_f16 x
+  def f32 (x: f32) = intrinsics.fpconv_f32_f16 x
+  def f64 (x: f64) = intrinsics.fpconv_f64_f16 x
+
+  def bool (x: bool) = if x then 1f16 else 0f16
+
+  def from_fraction (x: i64) (y: i64) = i64 x / i64 y
+  def to_i64 (x: f16) = intrinsics.fptosi_f16_i64 x
+  def to_f64 (x: f16) = intrinsics.fpconv_f16_f64 x
+
+  def (x: f16) == (y: f16) = intrinsics.eq_f16 (x, y)
+  def (x: f16) < (y: f16) = intrinsics.lt16 (x, y)
+  def (x: f16) > (y: f16) = intrinsics.lt16 (y, x)
+  def (x: f16) <= (y: f16) = intrinsics.le16 (x, y)
+  def (x: f16) >= (y: f16) = intrinsics.le16 (y, x)
+  def (x: f16) != (y: f16) = !(x == y)
+
+  def neg (x: t) = -x
+  def recip (x: t) = 1/x
+  def max (x: t) (y: t) = intrinsics.fmax16 (x, y)
+  def min (x: t) (y: t) = intrinsics.fmin16 (x, y)
+
+  def sgn (x: f16) = intrinsics.fsignum16 x
+  def abs (x: f16) = intrinsics.fabs16 x
+
+  def sqrt (x: f16) = intrinsics.sqrt16 x
+
+  def log (x: f16) = intrinsics.log16 x
+  def log2 (x: f16) = intrinsics.log2_16 x
+  def log10 (x: f16) = intrinsics.log10_16 x
+  def exp (x: f16) = intrinsics.exp16 x
+  def sin (x: f16) = intrinsics.sin16 x
+  def cos (x: f16) = intrinsics.cos16 x
+  def tan (x: f16) = intrinsics.tan16 x
+  def acos (x: f16) = intrinsics.acos16 x
+  def asin (x: f16) = intrinsics.asin16 x
+  def atan (x: f16) = intrinsics.atan16 x
+  def sinh (x: f16) = intrinsics.sinh16 x
+  def cosh (x: f16) = intrinsics.cosh16 x
+  def tanh (x: f16) = intrinsics.tanh16 x
+  def acosh (x: f16) = intrinsics.acosh16 x
+  def asinh (x: f16) = intrinsics.asinh16 x
+  def atanh (x: f16) = intrinsics.atanh16 x
+  def atan2 (x: f16) (y: f16) = intrinsics.atan2_16 (x, y)
+  def hypot (x: f16) (y: f16) = intrinsics.hypot16 (x, y)
+  def gamma = intrinsics.gamma16
+  def lgamma = intrinsics.lgamma16
+
+  def lerp v0 v1 t = intrinsics.lerp16 (v0,v1,t)
+  def fma a b c = intrinsics.fma16 (a,b,c)
+  def mad a b c = intrinsics.mad16 (a,b,c)
+
+  def ceil = intrinsics.ceil16
+  def floor = intrinsics.floor16
+  def trunc (x: f16) : f16 = i16 (i16m.f16 x)
+
+  def round = intrinsics.round16
+
+  def to_bits (x: f16): u16 = u16m.i16 (intrinsics.to_bits16 x)
+  def from_bits (x: u16): f16 = intrinsics.from_bits16 (intrinsics.sign_i16 x)
+
+  def num_bits = 16i32
+  def get_bit (bit: i32) (x: t) = u16m.get_bit bit (to_bits x)
+  def set_bit (bit: i32) (x: t) (b: i32) = from_bits (u16m.set_bit bit (to_bits x) b)
+
+  def isinf (x: f16) = intrinsics.isinf16 x
+  def isnan (x: f16) = intrinsics.isnan16 x
+
+  def inf = 1f16 / 0f16
+  def nan = 0f16 / 0f16
+
+  def highest = inf
+  def lowest = -inf
+  def epsilon = 1.1920929e-7f16
+
+  def pi = f64 f64m.pi
+  def e = f64 f64m.e
+
+  def sum = reduce (+) (i32 0)
+  def product = reduce (*) (i32 1)
+  def maximum = reduce max lowest
+  def minimum = reduce min highest
 }
diff --git a/prelude/prelude.fut b/prelude/prelude.fut
--- a/prelude/prelude.fut
+++ b/prelude/prelude.fut
@@ -7,33 +7,33 @@
 open import "functional"
 
 -- | Create single-precision float from integer.
-let r32 (x: i32): f32 = f32.i32 x
+def r32 (x: i32): f32 = f32.i32 x
 -- | Create integer from single-precision float.
-let t32 (x: f32): i32 = i32.f32 x
+def t32 (x: f32): i32 = i32.f32 x
 
 -- | Create double-precision float from integer.
-let r64 (x: i32): f64 = f64.i32 x
+def r64 (x: i32): f64 = f64.i32 x
 -- | Create integer from double-precision float.
-let t64 (x: f64): i32 = i32.f64 x
+def t64 (x: f64): i32 = i32.f64 x
 
 -- | Negate a boolean.  `not x` is the same as `!x`.  This function is
 -- mostly useful for passing to `map
-let not (x: bool): bool = !x
+def not (x: bool): bool = !x
 
 -- | Semantically just identity, but serves as an optimisation
 -- inhibitor.  The compiler will treat this function as a black box.
 -- You can use this to work around optimisation deficiencies (or
 -- bugs), although it should hopefully rarely be necessary.
 -- Deprecated: use `#[opaque]` attribute instead.
-let opaque 't (x: t): t =
+def opaque 't (x: t): t =
   #[opaque] x
 
 -- | Semantically just identity, but at runtime, the argument value
 -- will be printed.  Deprecated: use `#[trace]` attribute instead.
-let trace 't (x: t): t =
+def trace 't (x: t): t =
   #[trace(trace)] x
 
 -- | Semantically just identity, but acts as a break point in
 -- `futhark repl`.  Deprecated: use `#[break]` attribute instead.
-let break 't (x: t): t =
+def break 't (x: t): t =
   #[break] x
diff --git a/prelude/soacs.fut b/prelude/soacs.fut
--- a/prelude/soacs.fut
+++ b/prelude/soacs.fut
@@ -47,7 +47,7 @@
 -- **Work:** *O(n ✕ W(f))*
 --
 -- **Span:** *O(S(f))*
-let map 'a [n] 'x (f: a -> x) (as: [n]a): *[n]x =
+def map 'a [n] 'x (f: a -> x) (as: [n]a): *[n]x =
   intrinsics.map (f, as) :> *[n]x
 
 -- | Apply the given function to each element of a single array.
@@ -55,7 +55,7 @@
 -- **Work:** *O(n ✕ W(f))*
 --
 -- **Span:** *O(S(f))*
-let map1 'a [n] 'x (f: a -> x) (as: [n]a): *[n]x =
+def map1 'a [n] 'x (f: a -> x) (as: [n]a): *[n]x =
   map f as
 
 -- | As `map1`@term, but with one more array.
@@ -63,7 +63,7 @@
 -- **Work:** *O(n ✕ W(f))*
 --
 -- **Span:** *O(S(f))*
-let map2 'a 'b [n] 'x (f: a -> b -> x) (as: [n]a) (bs: [n]b): *[n]x =
+def map2 'a 'b [n] 'x (f: a -> b -> x) (as: [n]a) (bs: [n]b): *[n]x =
   map (\(a, b) -> f a b) (zip2 as bs)
 
 -- | As `map2`@term, but with one more array.
@@ -71,7 +71,7 @@
 -- **Work:** *O(n ✕ W(f))*
 --
 -- **Span:** *O(S(f))*
-let map3 'a 'b 'c [n] 'x (f: a -> b -> c -> x) (as: [n]a) (bs: [n]b) (cs: [n]c): *[n]x =
+def map3 'a 'b 'c [n] 'x (f: a -> b -> c -> x) (as: [n]a) (bs: [n]b) (cs: [n]c): *[n]x =
   map (\(a, b, c) -> f a b c) (zip3 as bs cs)
 
 -- | As `map3`@term, but with one more array.
@@ -79,7 +79,7 @@
 -- **Work:** *O(n ✕ W(f))*
 --
 -- **Span:** *O(S(f))*
-let map4 'a 'b 'c 'd [n] 'x (f: a -> b -> c -> d -> x) (as: [n]a) (bs: [n]b) (cs: [n]c) (ds: [n]d): *[n]x =
+def map4 'a 'b 'c 'd [n] 'x (f: a -> b -> c -> d -> x) (as: [n]a) (bs: [n]b) (cs: [n]c) (ds: [n]d): *[n]x =
   map (\(a, b, c, d) -> f a b c d) (zip4 as bs cs ds)
 
 -- | As `map3`@term, but with one more array.
@@ -87,7 +87,7 @@
 -- **Work:** *O(n ✕ W(f))*
 --
 -- **Span:** *O(S(f))*
-let map5 'a 'b 'c 'd 'e [n] 'x (f: a -> b -> c -> d -> e -> x) (as: [n]a) (bs: [n]b) (cs: [n]c) (ds: [n]d) (es: [n]e): *[n]x =
+def map5 'a 'b 'c 'd 'e [n] 'x (f: a -> b -> c -> d -> e -> x) (as: [n]a) (bs: [n]b) (cs: [n]c) (ds: [n]d) (es: [n]e): *[n]x =
   map (\(a, b, c, d, e) -> f a b c d e) (zip5 as bs cs ds es)
 
 -- | Reduce the array `as` with `op`, with `ne` as the neutral
@@ -103,7 +103,7 @@
 --
 -- Note that the complexity implies that parallelism in the combining
 -- operator will *not* be exploited.
-let reduce [n] 'a (op: a -> a -> a) (ne: a) (as: [n]a): a =
+def reduce [n] 'a (op: a -> a -> a) (ne: a) (as: [n]a): a =
   intrinsics.reduce (op, ne, as)
 
 -- | As `reduce`, but the operator must also be commutative.  This is
@@ -114,7 +114,7 @@
 -- **Work:** *O(n ✕ W(op))*
 --
 -- **Span:** *O(log(n) ✕ W(op))*
-let reduce_comm [n] 'a (op: a -> a -> a) (ne: a) (as: [n]a): a =
+def reduce_comm [n] 'a (op: a -> a -> a) (ne: a) (as: [n]a): a =
   intrinsics.reduce_comm (op, ne, as)
 
 -- | `reduce_by_index dest f ne is as` returns `dest`, but with each
@@ -132,7 +132,7 @@
 --
 -- In practice, the *O(n)* behaviour only occurs if *m* is also very
 -- large.
-let reduce_by_index 'a [m] [n] (dest : *[m]a) (f : a -> a -> a) (ne : a) (is : [n]i64) (as : [n]a) : *[m]a =
+def reduce_by_index 'a [m] [n] (dest : *[m]a) (f : a -> a -> a) (ne : a) (is : [n]i64) (as : [n]a) : *[m]a =
   intrinsics.hist (1, dest, f, ne, is, as) :> *[m]a
 
 -- | Inclusive prefix scan.  Has the same caveats with respect to
@@ -141,7 +141,7 @@
 -- **Work:** *O(n ✕ W(op))*
 --
 -- **Span:** *O(log(n) ✕ W(op))*
-let scan [n] 'a (op: a -> a -> a) (ne: a) (as: [n]a): *[n]a =
+def scan [n] 'a (op: a -> a -> a) (ne: a) (as: [n]a): *[n]a =
   intrinsics.scan (op, ne, as) :> *[n]a
 
 -- | Remove all those elements of `as` that do not satisfy the
@@ -150,7 +150,7 @@
 -- **Work:** *O(n ✕ W(p))*
 --
 -- **Span:** *O(log(n) ✕ W(p))*
-let filter [n] 'a (p: a -> bool) (as: [n]a): *[]a =
+def filter [n] 'a (p: a -> bool) (as: [n]a): *[]a =
   let (as', is) = intrinsics.partition (1, \x -> if p x then 0 else 1, as)
   in as'[:is[0]]
 
@@ -160,7 +160,7 @@
 -- **Work:** *O(n ✕ W(p))*
 --
 -- **Span:** *O(log(n) ✕ W(p))*
-let partition [n] 'a (p: a -> bool) (as: [n]a): ([]a, []a) =
+def partition [n] 'a (p: a -> bool) (as: [n]a): ([]a, []a) =
   let p' x = if p x then 0 else 1
   let (as', is) = intrinsics.partition (2, p', as)
   in (as'[0:is[0]], as'[is[0]:n])
@@ -170,7 +170,7 @@
 -- **Work:** *O(n ✕ (W(p1) + W(p2)))*
 --
 -- **Span:** *O(log(n) ✕ (W(p1) + W(p2)))*
-let partition2 [n] 'a (p1: a -> bool) (p2: a -> bool) (as: [n]a): ([]a, []a, []a) =
+def partition2 [n] 'a (p1: a -> bool) (p2: a -> bool) (as: [n]a): ([]a, []a, []a) =
   let p' x = if p1 x then 0 else if p2 x then 1 else 2
   let (as', is) = intrinsics.partition (3, p', as)
   in (as'[0:is[0]], as'[is[0]:is[0]+is[1]], as'[is[0]+is[1]:n])
@@ -190,7 +190,7 @@
 -- **Work:** *O(n ✕ W(op) + W(f))*
 --
 -- **Span:** *O(log(n) ✕ W(op))*
-let reduce_stream [n] 'a 'b (op: b -> b -> b) (f: (k: i64) -> [k]a -> b) (as: [n]a): b =
+def reduce_stream [n] 'a 'b (op: b -> b -> b) (f: (k: i64) -> [k]a -> b) (as: [n]a): b =
   intrinsics.reduce_stream (op, f, as)
 
 -- | As `reduce_stream`@term, but the chunks do not necessarily
@@ -200,7 +200,7 @@
 -- **Work:** *O(n ✕ W(op) + W(f))*
 --
 -- **Span:** *O(log(n) ✕ W(op))*
-let reduce_stream_per [n] 'a 'b (op: b -> b -> b) (f: (k: i64) -> [k]a -> b) (as: [n]a): b =
+def reduce_stream_per [n] 'a 'b (op: b -> b -> b) (f: (k: i64) -> [k]a -> b) (as: [n]a): b =
   intrinsics.reduce_stream_per (op, f, as)
 
 -- | Similar to `reduce_stream`@term, except that each chunk must produce
@@ -210,7 +210,7 @@
 -- **Work:** *O(n ✕ W(f))*
 --
 -- **Span:** *O(S(f))*
-let map_stream [n] 'a 'b (f: (k: i64) -> [k]a -> [k]b) (as: [n]a): *[n]b =
+def map_stream [n] 'a 'b (f: (k: i64) -> [k]a -> [k]b) (as: [n]a): *[n]b =
   intrinsics.map_stream (f, as) :> *[n]b
 
 -- | Similar to `map_stream`@term, but the chunks do not necessarily
@@ -220,7 +220,7 @@
 -- **Work:** *O(n ✕ W(f))*
 --
 -- **Span:** *O(S(f))*
-let map_stream_per [n] 'a 'b (f: (k: i64) -> [k]a -> [k]b) (as: [n]a): *[n]b =
+def map_stream_per [n] 'a 'b (f: (k: i64) -> [k]a -> [k]b) (as: [n]a): *[n]b =
   intrinsics.map_stream_per (f, as) :> *[n]b
 
 -- | Return `true` if the given function returns `true` for all
@@ -229,7 +229,7 @@
 -- **Work:** *O(n ✕ W(f))*
 --
 -- **Span:** *O(log(n) + S(f))*
-let all [n] 'a (f: a -> bool) (as: [n]a): bool =
+def all [n] 'a (f: a -> bool) (as: [n]a): bool =
   reduce (&&) true (map f as)
 
 -- | Return `true` if the given function returns `true` for any
@@ -238,7 +238,7 @@
 -- **Work:** *O(n ✕ W(f))*
 --
 -- **Span:** *O(log(n) + S(f))*
-let any [n] 'a (f: a -> bool) (as: [n]a): bool =
+def any [n] 'a (f: a -> bool) (as: [n]a): bool =
   reduce (||) false (map f as)
 
 -- | `scatter as is vs` calculates the equivalent of this imperative
@@ -269,7 +269,7 @@
 -- **Work:** *O(n)*
 --
 -- **Span:** *O(1)*
-let scatter 't [m] [n] (dest: *[m]t) (is: [n]i64) (vs: [n]t): *[m]t =
+def scatter 't [m] [n] (dest: *[m]t) (is: [n]i64) (vs: [n]t): *[m]t =
   intrinsics.scatter (dest, is, vs) :> *[m]t
 
 -- | `scatter_2d as is vs` is the equivalent of a `scatter` on a 2-dimensional
@@ -278,7 +278,7 @@
 -- **Work:** *O(n)*
 --
 -- **Span:** *O(1)*
-let scatter_2d 't [m] [n] [l] (dest: *[m][n]t) (is: [l](i64, i64)) (vs: [l]t): *[m][n]t =
+def scatter_2d 't [m] [n] [l] (dest: *[m][n]t) (is: [l](i64, i64)) (vs: [l]t): *[m][n]t =
   intrinsics.scatter_2d (dest, is, vs) :> *[m][n]t
 
 -- | `scatter_3d as is vs` is the equivalent of a `scatter` on a 3-dimensional
@@ -287,5 +287,5 @@
 -- **Work:** *O(n)*
 --
 -- **Span:** *O(1)*
-let scatter_3d 't [m] [n] [o] [l] (dest: *[m][n][o]t) (is: [l](i64, i64, i64)) (vs: [l]t): *[m][n][o]t =
+def scatter_3d 't [m] [n] [o] [l] (dest: *[m][n][o]t) (is: [l](i64, i64, i64)) (vs: [l]t): *[m][n][o]t =
   intrinsics.scatter_3d (dest, is, vs) :> *[m][n][o]t
diff --git a/prelude/zip.fut b/prelude/zip.fut
--- a/prelude/zip.fut
+++ b/prelude/zip.fut
@@ -10,51 +10,51 @@
 -- We need a map to define some of the zip variants, but this file is
 -- depended upon by soacs.fut.  So we just define a quick-and-dirty
 -- internal one here that uses the intrinsic version.
-local let internal_map 'a [n] 'x (f: a -> x) (as: [n]a): [n]x =
+local def internal_map 'a [n] 'x (f: a -> x) (as: [n]a): [n]x =
   intrinsics.map (f, as) :> [n]x
 
 -- | Construct an array of pairs from two arrays.
-let zip [n] 'a 'b (as: [n]a) (bs: [n]b): *[n](a,b) =
+def zip [n] 'a 'b (as: [n]a) (bs: [n]b): *[n](a,b) =
   intrinsics.zip (as, bs) :> *[n](a,b)
 
 -- | Construct an array of pairs from two arrays.
-let zip2 [n] 'a 'b (as: [n]a) (bs: [n]b): *[n](a,b) =
+def zip2 [n] 'a 'b (as: [n]a) (bs: [n]b): *[n](a,b) =
   zip as bs :> *[n](a,b)
 
 -- | As `zip2`@term, but with one more array.
-let zip3 [n] 'a 'b 'c (as: [n]a) (bs: [n]b) (cs: [n]c): *[n](a,b,c) =
+def zip3 [n] 'a 'b 'c (as: [n]a) (bs: [n]b) (cs: [n]c): *[n](a,b,c) =
   internal_map (\(a,(b,c)) -> (a,b,c)) (zip as (zip2 bs cs))
 
 -- | As `zip3`@term, but with one more array.
-let zip4 [n] 'a 'b 'c 'd (as: [n]a) (bs: [n]b) (cs: [n]c) (ds: [n]d): *[n](a,b,c,d) =
+def zip4 [n] 'a 'b 'c 'd (as: [n]a) (bs: [n]b) (cs: [n]c) (ds: [n]d): *[n](a,b,c,d) =
   internal_map (\(a,(b,c,d)) -> (a,b,c,d)) (zip as (zip3 bs cs ds))
 
 -- | As `zip4`@term, but with one more array.
-let zip5 [n] 'a 'b 'c 'd 'e (as: [n]a) (bs: [n]b) (cs: [n]c) (ds: [n]d) (es: [n]e): *[n](a,b,c,d,e) =
+def zip5 [n] 'a 'b 'c 'd 'e (as: [n]a) (bs: [n]b) (cs: [n]c) (ds: [n]d) (es: [n]e): *[n](a,b,c,d,e) =
   internal_map (\(a,(b,c,d,e)) -> (a,b,c,d,e)) (zip as (zip4 bs cs ds es))
 
 -- | Turn an array of pairs into two arrays.
-let unzip [n] 'a 'b (xs: [n](a,b)): ([n]a, [n]b) =
+def unzip [n] 'a 'b (xs: [n](a,b)): ([n]a, [n]b) =
   intrinsics.unzip xs :> ([n]a, [n]b)
 
 -- | Turn an array of pairs into two arrays.
-let unzip2 [n] 'a 'b (xs: [n](a,b)): ([n]a, [n]b) =
+def unzip2 [n] 'a 'b (xs: [n](a,b)): ([n]a, [n]b) =
   unzip xs
 
 -- | As `unzip2`@term, but with one more array.
-let unzip3 [n] 'a 'b 'c (xs: [n](a,b,c)): ([n]a, [n]b, [n]c) =
+def unzip3 [n] 'a 'b 'c (xs: [n](a,b,c)): ([n]a, [n]b, [n]c) =
   let (as, bcs) = unzip (internal_map (\(a,b,c) -> (a,(b,c))) xs)
   let (bs, cs) = unzip bcs
   in (as, bs, cs)
 
 -- | As `unzip3`@term, but with one more array.
-let unzip4 [n] 'a 'b 'c 'd (xs: [n](a,b,c,d)): ([n]a, [n]b, [n]c, [n]d) =
+def unzip4 [n] 'a 'b 'c 'd (xs: [n](a,b,c,d)): ([n]a, [n]b, [n]c, [n]d) =
   let (as, bs, cds) = unzip3 (internal_map (\(a,b,c,d) -> (a,b,(c,d))) xs)
   let (cs, ds) = unzip cds
   in (as, bs, cs, ds)
 
 -- | As `unzip4`@term, but with one more array.
-let unzip5 [n] 'a 'b 'c 'd 'e (xs: [n](a,b,c,d,e)): ([n]a, [n]b, [n]c, [n]d, [n]e) =
+def unzip5 [n] 'a 'b 'c 'd 'e (xs: [n](a,b,c,d,e)): ([n]a, [n]b, [n]c, [n]d, [n]e) =
   let (as, bs, cs, des) = unzip4 (internal_map (\(a,b,c,d,e) -> (a,b,c,(d,e))) xs)
   let (ds, es) = unzip des
   in (as, bs, cs, ds, es)
diff --git a/src/Futhark/CLI/Defs.hs b/src/Futhark/CLI/Defs.hs
new file mode 100644
--- /dev/null
+++ b/src/Futhark/CLI/Defs.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+-- | @futhark defs@
+module Futhark.CLI.Defs (main) where
+
+import Data.List (isPrefixOf)
+import qualified Data.Sequence as Seq
+import qualified Data.Text as T
+import qualified Data.Text.IO as T
+import Futhark.Compiler
+import Futhark.Util.Loc
+import Futhark.Util.Options
+import Language.Futhark
+
+isBuiltin :: String -> Bool
+isBuiltin = ("prelude/" `isPrefixOf`)
+
+data DefKind = Value | Module | ModuleType | Type
+
+data Def = Def DefKind Name Loc
+
+kindText :: DefKind -> T.Text
+kindText Value = "value"
+kindText Module = "module"
+kindText ModuleType = "module type"
+kindText Type = "type"
+
+printDef :: Def -> IO ()
+printDef (Def k name loc) = do
+  T.putStrLn $ T.unwords [kindText k, nameToText name, T.pack (locStr loc)]
+
+defsInProg :: UncheckedProg -> Seq.Seq Def
+defsInProg = foldMap defsInDec . progDecs
+  where
+    defsInDec (ValDec vb) =
+      Seq.singleton $ Def Value (valBindName vb) (locOf vb)
+    defsInDec (TypeDec tb) =
+      Seq.singleton $ Def Type (typeAlias tb) (locOf tb)
+    defsInDec (LocalDec d _) = defsInDec d
+    defsInDec (OpenDec me _) = defsInModExp me
+    defsInDec (ModDec mb) = defsInModExp $ modExp mb
+    defsInDec SigDec {} = mempty
+    defsInDec ImportDec {} = mempty
+
+    defsInModExp ModVar {} = mempty
+    defsInModExp (ModParens me _) = defsInModExp me
+    defsInModExp ModImport {} = mempty
+    defsInModExp (ModDecs ds _) = foldMap defsInDec ds
+    defsInModExp (ModApply me1 me2 _ _ _) = defsInModExp me1 <> defsInModExp me2
+    defsInModExp (ModAscript me _ _ _) = defsInModExp me
+    defsInModExp (ModLambda _ _ me _) = defsInModExp me
+
+-- | Run @futhark defs@.
+main :: String -> [String] -> IO ()
+main = mainWithOptions () [] "program" $ \args () ->
+  case args of
+    [file] -> Just $ do
+      prog <- readUntypedProgramOrDie file
+      mapM_ printDef . foldMap (defsInProg . snd) $
+        filter (not . isBuiltin . fst) prog
+    _ -> Nothing
diff --git a/src/Futhark/Pass/ExtractKernels/Intragroup.hs b/src/Futhark/Pass/ExtractKernels/Intragroup.hs
--- a/src/Futhark/Pass/ExtractKernels/Intragroup.hs
+++ b/src/Futhark/Pass/ExtractKernels/Intragroup.hs
@@ -81,7 +81,7 @@
 
   ((intra_avail_par, kspace, read_input_stms), prelude_stms) <- lift $
     runBuilder $ do
-      let foldBinOp' _ [] = eSubExp $ intConst Int64 0
+      let foldBinOp' _ [] = eSubExp $ intConst Int64 1
           foldBinOp' bop (x : xs) = foldBinOp bop x xs
       ws_min <-
         mapM (letSubExp "one_intra_par_min" <=< foldBinOp' (Mul Int64 OverflowUndef)) $
@@ -91,8 +91,9 @@
           filter (not . null) wss_avail
 
       -- The amount of parallelism available *in the worst case* is
-      -- equal to the smallest parallel loop.
-      intra_avail_par <- letSubExp "intra_avail_par" =<< foldBinOp' (SMin Int64) ws_avail
+      -- equal to the smallest parallel loop, or *at least* 1.
+      intra_avail_par <-
+        letSubExp "intra_avail_par" =<< foldBinOp' (SMin Int64) ws_avail
 
       -- The group size is either the maximum of the minimum parallelism
       -- exploited, or the desired parallelism (bounded by the max group
diff --git a/src/Language/Futhark/Parser/Lexer.x b/src/Language/Futhark/Parser/Lexer.x
--- a/src/Language/Futhark/Parser/Lexer.x
+++ b/src/Language/Futhark/Parser/Lexer.x
@@ -137,6 +137,7 @@
     "if"           -> IF
     "then"         -> THEN
     "else"         -> ELSE
+    "def"          -> DEF
     "let"          -> LET
     "loop"         -> LOOP
     "in"           -> IN
@@ -344,6 +345,7 @@
            | IF
            | THEN
            | ELSE
+           | DEF
            | LET
            | LOOP
            | IN
diff --git a/src/Language/Futhark/Parser/Parser.y b/src/Language/Futhark/Parser/Parser.y
--- a/src/Language/Futhark/Parser/Parser.y
+++ b/src/Language/Futhark/Parser/Parser.y
@@ -61,6 +61,7 @@
       then            { L $$ THEN }
       else            { L $$ ELSE }
       let             { L $$ LET }
+      def             { L $$ DEF }
       loop            { L $$ LOOP }
       in              { L $$ IN }
       match           { L $$ MATCH }
@@ -388,7 +389,7 @@
      | '(' BindingBinOp ')' { ($2, $1) }
 
 Val    :: { ValBindBase NoInfo Name }
-Val     : let BindingId TypeParams FunParams maybeAscription(TypeExpDecl) '=' Exp
+Val     : def BindingId TypeParams FunParams maybeAscription(TypeExpDecl) '=' Exp
           { let (name, _) = $2
             in ValBind Nothing name (fmap declaredType $5) NoInfo
                $3 $4 $7 Nothing mempty (srcspan $1 $>)
@@ -399,6 +400,17 @@
             in ValBind (Just NoInfo) name (fmap declaredType $5) NoInfo
                $3 $4 $7 Nothing mempty (srcspan $1 $>) }
 
+        | def FunParam BindingBinOp FunParam maybeAscription(TypeExpDecl) '=' Exp
+          { ValBind Nothing $3 (fmap declaredType $5) NoInfo [] [$2,$4] $7
+            Nothing mempty (srcspan $1 $>)
+          }
+
+        -- The next two for backwards compatibility.
+        | let BindingId TypeParams FunParams maybeAscription(TypeExpDecl) '=' Exp
+          { let (name, _) = $2
+            in ValBind Nothing name (fmap declaredType $5) NoInfo
+               $3 $4 $7 Nothing mempty (srcspan $1 $>)
+          }
         | let FunParam BindingBinOp FunParam maybeAscription(TypeExpDecl) '=' Exp
           { ValBind Nothing $3 (fmap declaredType $5) NoInfo [] [$2,$4] $7
             Nothing mempty (srcspan $1 $>)
@@ -737,7 +749,9 @@
 LetBody :: { UncheckedExp }
     : in Exp %prec letprec { $2 }
     | LetExp %prec letprec { $1 }
-    | error {% throwError "Unexpected end of file - missing \"in\"?" }
+    | def {% parseErrorAt $1 (Just "Unexpected \"def\" - missing \"in\"?") }
+    | type {% parseErrorAt $1 (Just "Unexpected \"type\" - missing \"in\"?") }
+    | module {% parseErrorAt $1 (Just "Unexpected \"module\" - missing \"in\"?") }
 
 MatchExp :: { UncheckedExp }
           : match Exp Cases
diff --git a/src/Language/Futhark/Pretty.hs b/src/Language/Futhark/Pretty.hs
--- a/src/Language/Futhark/Pretty.hs
+++ b/src/Language/Futhark/Pretty.hs
@@ -468,7 +468,7 @@
     where
       fun
         | isJust entry = "entry"
-        | otherwise = "let"
+        | otherwise = "def"
       retdecl' = case (ppr <$> unAnnot rettype) `mplus` (ppr <$> retdecl) of
         Just rettype' -> colon <+> align rettype'
         Nothing -> mempty
diff --git a/src/futhark.hs b/src/futhark.hs
--- a/src/futhark.hs
+++ b/src/futhark.hs
@@ -16,6 +16,7 @@
 import qualified Futhark.CLI.Check as Check
 import qualified Futhark.CLI.Datacmp as Datacmp
 import qualified Futhark.CLI.Dataset as Dataset
+import qualified Futhark.CLI.Defs as Defs
 import qualified Futhark.CLI.Dev as Dev
 import qualified Futhark.CLI.Doc as Doc
 import qualified Futhark.CLI.Literate as Literate
@@ -69,6 +70,7 @@
       ("imports", (Misc.mainImports, "Print all non-builtin imported Futhark files.")),
       ("hash", (Misc.mainHash, "Print hash of program AST.")),
       ("autotune", (Autotune.main, "Autotune threshold parameters.")),
+      ("defs", (Defs.main, "Show location and name of all definitions.")),
       ("query", (Query.main, "Query semantic information about program.")),
       ("literate", (Literate.main, "Process a literate Futhark program."))
     ]