From 6a7d65d4210728147c5f5a838181ec914f0271b0 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Wed, 16 Mar 2022 18:40:12 +0100
Subject: [PATCH] use :::aside instead of <aside>

---
 posts/2022-03-14-digitle-in-maude.md | 82 ++++++++++++++++------------
 1 file changed, 47 insertions(+), 35 deletions(-)

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.
 
-<aside>
-  **why is importing called `protecting`?** in maude, sorts (approximately,
-  types) aren't necessarily closed. you can add a new constructor, or equations
-  between constructor forms, at any time. unlike in languages like haskell or
-  rust, constructors don't have to be _free_, which means you can have equations
-  like `s (s (s (s z))) = z` and pow you've got $\mathbb{Z}/4\mathbb{Z}$.
+:::aside
+**why is importing called `protecting`?** in maude, sorts (approximately,
+types) aren't necessarily closed. you can add a new constructor, or equations
+between constructor forms, at any time. unlike in languages like haskell or
+rust, constructors don't have to be _free_, which means you can have equations
+between them. like to get `ℤ/4ℤ` you can just do something like
 
-  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.
+```maude
+fmod NAT4 is
+  including NAT .
+  eq 4 = 0 .
+endfm
+```
 
-  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
-</aside>
+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.
-</aside>
+:::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`.
-</aside>
+:::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).
-</aside>
+:::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.
-</aside>
+:::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