diff --git a/posts/2022-03-14-digitle-in-maude.md b/posts/2022-03-14-digitle-in-maude.md
index 3661133..c79ff0f 100644
--- a/posts/2022-03-14-digitle-in-maude.md
+++ b/posts/2022-03-14-digitle-in-maude.md
@@ -40,24 +40,31 @@ going into one. since digitle involves numbers, i'm also importing the `NAT`
module, and saying that any time `M` or `N` show up in equations or rewrite
rules they stand for single numbers.
-
+but when you're importing a module, most of the time you don't want to do any
+of that. so there are three ways of importing a module to express how much you
+intend to mess with it. `protecting` says you are not adding new constructors
+or conflating existing ones. `extending` lets you add new constructors, but
+not new equations. `including` lets you do whatever. since i'm just using
+_normal_ numbers, `protecting` is what i want.
+
+an important caveat is that it is not possible for maude itself to check you
+are telling the truth here, but it can ask `yices` or `cvc4` for help. please
+don't press me for more detail i have never used this
+:::
the first thing i need is a ~~type~~ sort for the pool of numbers we currently
have. it's a _multiset_: the number of copies of each number matters, but the
@@ -93,13 +100,13 @@ mean, so later when i have some equations and rewrite rules that match on the
beginning of a list, it knows that it can actually pick those numbers from
_anywhere_, without needing extra rules to shuffle the list around manually.
-
+:::aside
+**the name `__` is pretty weird!** generally operator names are written with an
+underscore where the arguments go, so the name of the addition operator is
+`_+_`. in this case, there _is_ no operator, it's just two things next to each
+other (in a context where a `Pool` value is expected, anyway), so it's just
+two underscores.
+:::
from here, we *could* just define the rewrite rules and be done. something like
this would work:
@@ -111,9 +118,14 @@ rl [mul] : M N => M * N .
crl [div] : M N => M quo N if M rem N = 0 .
```
-
+:::aside
+**`sd`** is "symmetric difference"---e.g. `sd(1, 4) = sd(4, 1) = 3`. \
+(it is also [a declaration form][sd] which is why it's purple.
+i don't know how to distinguish the two in pandoc/kate's syntax highlighting
+format sorry)
+
+[sd]: https://maude.lcc.uma.es/maude321-manual-html/maude-manualch10.html
+:::
the first three rules just pick two numbers from our pool (any two, because of
`comm`; they don't have to be next to each other), and replace them with the
@@ -200,10 +212,10 @@ op _,_ : Steps Steps -> Steps [assoc id: nil prec 20] .
var Ss : Steps .
```
-
+:::aside
+**`prec N`** is parsing/printing precedence (higher is looser, same as coq,
+opposite of haskell/agda/idris).
+:::
so solution traces are written like
`2 + 9 → 11,4 × 8 → 32,11 × 75 → 825,825 - 32 → 793`
@@ -235,11 +247,11 @@ eq (N Ps & Ss) has N = true .
eq S has N = false [otherwise] .
```
-
+:::aside
+it could even skip the `false` line with a slightly different signature but
+then i would have to explain more about the sort & kind system... this is good
+enough.
+:::
the new rewrite rules (delete the other ones) have the same behaviour for the