@@ -98,14 +98,16 @@ and is matched up with the appropriate type of data (often more
9898The `%clhp` is produced from the rune `:-` (i.e. "colhep"). The 2 and
999917 have each been parsed as `%sand`-tagged hoons, which represent
100100atoms (in this case each with an aura of `%ud`, i.e. unsigned
101−decimal). To parse Hoon source into a hoon AST, use `ream` on a `cord`
102−containing Hoon source, e.g.:
101+decimal).
102+
103+To parse Hoon source into a hoon AST, use `ream` on a `cord`
104+containing Hoon source, try the following in `dojo`:
103105
104106```
105107(ream ':+(12 7 %a)')
106108```
107109
108−Try the above in the `:dojo` to get:
110+The result should be:
109111
110112```
111113[%clls p=[%sand p=%ud q=12] q=[%sand p=%ud q=7] r=[%rock p=%tas q=97]]
@@ -116,19 +118,14 @@ Try the above in the `:dojo` to get:
116118[`mint`](#mint) is the Hoon compiler. It maps a cell `[type hoon]`
117119to a cell `[type nock]`, where a [`type`](#type) is type
118120information, a [`hoon`](#hoon) is a parsed expression (AST), and a
119−`nock` is a Nock formula. `mint` accepts a type and a parsed
120−source expression; it produces a product type and an executable
121−formula.
122−
123−As part of the type-checking process, mint checks that the output
124−type "nests" within the input type, i.e. that the output type is a
125−subset of the input type. If not, mint halts with a `nest-fail`
126−crash.
121+`nock` is a Nock formula. `mint` takes as input the subject type
122+and a parsed source expression; it produces a product type and an
123+executable formula.
127124
128125Calculating the output type from the input `hoon` is called "type
129126inference". If you've used another typed functional language, like
130−Haskell, Hoon's type inference does the same job but with less
131−intelligence.
127+Haskell, the Hoon compiler's type inference does the same job but
128+with less intelligence.
132129
133130Haskell infers backward and forward; Hoon only infers forward.
134131Hoon can't figure out the type of a noun from how you use it,
@@ -140,15 +137,27 @@ which makes your program more readable anyway. Also, the dumber
140137the compiler, the easier it is for a dumb human to understand
141138what the compiler is thinking.
142139
143−To compile an example `hoon` from the last subsection into Nock,
144−try the following in `:dojo`:
140+The `mint` gate is inside the core `++ ut`, so call it using the
141+following syntax:
145142
146143```
147−(mint:ut %noun [%clhp p=[%sand p=%ud q=2] q=[%sand p=%ud q=17]])
144+(~(<gate> <core> <arg 1>) <arg 2> <arg 3>)
148145```
149146
150−The `%noun` is the input `type` for `mint`, and the tree after that
151−is the input `hoon`.
147+The `<gate>` is mint, the `<core>` is `ut`, `<arg 1>` is the subject
148+type, and `<arg 3>` is the parsed Hoon AST (i.e., a `hoon` from the
149+last section). What's `<arg 2>`? It's another piece of type
150+information. As part of the type-checking process, mint checks that
151+the output type "nests" within the input type, i.e. that the output
152+type is a subset of the input type. If not, mint halts with a
153+`nest-fail` crash.
154+
155+Let's compile an example `hoon` from the last subsection into Nock.
156+Try the following in `:dojo`:
157+
158+```
159+(~(mint ut %noun) %noun [%clhp p=[%sand p=%ud q=2] q=[%sand p=%ud q=17]])
160+```
152161
153162### <a name="type">`type`</a> (type, as range)
154163