@@ -1,4 +1,6 @@
11---
2+navhome: /docs
3+next: true
24sort: 3
35title: Glossary of Urbit Terms
46---
@@ -48,7 +50,7 @@ or `48.879`, whose parent is `~mun`, `0xef`, `239`. The parent of
4850
4951### Nock
5052
51−>Nock is a Turing-complete, non-lambda combinator function.
53+> Nock is a Turing-complete, non-lambda combinator function.
5254
5355- `noun`: an `atom` or a `cell`
5456- `atom`: any natural number
@@ -61,7 +63,7 @@ or `48.879`, whose parent is `~mun`, `0xef`, `239`. The parent of
6163
6264### Hoon
6365
64−>Hoon is a strict, higher-order typed functional language which compiles itself to Nock.
66+> Hoon is a strict, higher-order typed functional language which compiles itself to Nock.
6567
6668###### `span`: an inferred type
6769
@@ -110,7 +112,7 @@ The code (`battery`) is the head, the data (`payload`) is the tail. All code-dat
110112
111113*TODO: simplify*
112114
113−>When we call a `wet` `arm`, we're essentially using the `twig` as a macro. We are not generating new code for every call site; we are creating a new type analysis path, which works as if we expanded the callee with the caller's context.
115+> When we call a `wet` `arm`, we're essentially using the `twig` as a macro. We are not generating new code for every call site; we are creating a new type analysis path, which works as if we expanded the callee with the caller's context.
114116
115117- `dry`: polymorphic by means of *variance*
116118
@@ -144,17 +146,18 @@ A Hoon `atom` is a Nock `atom`, with two additional pieces of metadata (TODO: ?)
144146
145147###### `aura`: a soft `atom` type
146148
147−*alternately **odor***
149+*alternately `odor`*
148150
149151*TODO: write a short summary*
150152
151153*TODO: are `aura`s always `mold`s? just the built-in `aura`s?*
152154
153−>Auras are a lightweight, advisory representation of the units, semantics, and/or syntax of an `atom`. An `aura` is an atomic string; two auras are compatible if one is a prefix of the other.
154−
155−>For instance, @t means UTF-8 text (LSB low), @ta means ASCII text, and @tas means an ASCII symbol. @u means an unsigned integer, @ud an unsigned decimal, @ux an unsigned hexadecimal. You can use a @ud atom as a @u or vice versa, but not as a @tas.
156−
157−>Auras are truly soft; you can turn any `aura` into any other, statically, by casting through the empty `aura` `@`. Hoon is not dependently typed and can't statically enforce data constraints (for example, it can't enforce that a `@tas` is really a symbol).
155+> Auras are a lightweight, advisory representation of the units, semantics, and/or syntax of an `atom`. An `aura` is an atomic string; two auras are compatible if one is a prefix of the other.
156+>
157+> For instance, @t means UTF-8 text (LSB low), @ta means ASCII text, and @tas means an ASCII symbol. @u means an unsigned integer, @ud an unsigned decimal, @ux an unsigned hexadecimal. You can use a @ud atom as a @u or vice versa, but not as a @tas.
158+>
159+> Auras are truly soft; you can turn any `aura` into any other, statically, by casting through the empty `aura` `@`. Hoon is not dependently typed and can't statically enforce data constraints (for example, it can't enforce that a `@tas` is really a symbol).
160+>
158161
159162- `term` (`@tas`): a symbol - an atomic ASCII string which obeys symbol rules: lowercase and digit only, infix hyphen ("worm-case"), first character must be lowercase *(TODO: alphabetic?)*.
160163
@@ -227,10 +230,9 @@ A `face` is a `span` *(TODO: ?)* with a label (`@tas`) wrapped around it.
227230
228231### Arvo
229232
230−>Arvo is a nonpreemptive OS kernel, a single-threaded event interpreter.
233+> Arvo is a nonpreemptive OS kernel, a single-threaded event interpreter.
231234
232235- `mark`
233236- `generator`
234237
235238*... TODO*
236−