on master help sign in
nesting fix, bunting
commite0007c38999a7ca614ba481569a556a70817df75 authordrbeefsupreme <drbeefsupreme@discordja.net> dateTue 16 Mar 2021, 16:53 (6 years ago) parent8b34d79
1 file changed+27−7
hoon/reference/auras.md+27−7
hoon/reference/auras.md+27−7
@@ -8,13 +8,10 @@ Auras are system of nested "soft types" on [atoms](@/docs/glossary/atom.md) that
88are used to track metadata about how a particular atom is to be interpreted.
99This is used for type checking as well as pretty printing.
1010
11−A given aura nests under any aura whose name is a substring of the given aura,
12−i.e. `@ux` nests under `@u`, and all auras nest under the empty aura `@`. We
13−call auras "soft types" since this nesting behavior can be ignored - see
14−[below](#non-coercive).
15−
1611You can learn more about auras in [Hoon school](@/docs/hoon/hoon-school/atoms-auras-and-simple-types.md).
1712
13+### Table of Auras
14+
1815```
1916Aura Meaning Example Literal Syntax
2017-------------------------------------------------------------------------
@@ -52,6 +49,8 @@ Aura Meaning Example Literal Syntax
5249 @ux unsigned hexadecimal 0x5f5.e138
5350```
5451
52+### Bitwidth
53+
5554Capital letters at the end of auras indicate the bitwidth in binary powers of
5655two, starting from A.
5756
@@ -63,9 +62,22 @@ two, starting from A.
6362 @uvJ unsigned, 512-bit integer (frequently used for entropy)
6463```
6564
66−### Non-coercive
65+### Nesting
6766
68−Auras are non-coercive, but conversions may have to go via the empty aura, e.g.
67+A given aura nests under any aura whose name is a substring or extension of the
68+given aura:
69+```
70+> :- (~(nest ut [%atom %ud ~]) | [%atom %u ~])
71+ (~(nest ut [%atom %ud ~]) | [%atom %udx ~])
72+[%.y %.y]
73+```
74+but does not nest "sideways":
75+```
76+> (~(nest ut [%atom %ud ~]) | [%atom %ux ~])
77+%.n
78+```
79+We call auras "soft types" since this nesting behavior can be ignored. Auras are
80+non-coercive, but conversions may have to go via the empty aura, e.g.
6981```
7082> ^-(@ud ^-(@ 'foo'))
71837.303.014
@@ -75,3 +87,11 @@ This is implicitly done by the irregular form of `^-`.
7587> `@ud`'foo'
76887.303.014
7789```
90+
91+### Bunting
92+
93+The bunt value for all auras is 0 except for `@da`.
94+```
95+> *@da
96+~2000.1.1
97+```