diff --git a/Makefile b/Makefile
index 913b43a..87fdf3b 100644
--- a/Makefile
+++ b/Makefile
@@ -116,7 +116,7 @@ endef
upload: build
@echo "[upload]"
@rsync --recursive --partial --progress --copy-links \
- --compress --human-readable --hard-links --size-only \
+ --compress --human-readable --hard-links \
--delete --delete-after \
--rsh='ssh -l $(REMOTE_USER)' \
$(BUILDDIR)/ $(HOST):$(REMOTE_DIR)/
diff --git a/images/qt.svg b/images/qt.svg
new file mode 100644
index 0000000..a7caf28
--- /dev/null
+++ b/images/qt.svg
@@ -0,0 +1,128 @@
+
+
+
\ No newline at end of file
diff --git a/posts-wip/rainbow-quox.md b/posts-wip/rainbow-quox.md
deleted file mode 100644
index 84186c4..0000000
--- a/posts-wip/rainbow-quox.md
+++ /dev/null
@@ -1,274 +0,0 @@
----
-title: rainbow quox
-date: 2024-11-17
-tags: [computer, website, fursona]
-summary: q.t. colour scheme generator
-...
-
-so how about that regular posting, huh. ha ha ha
-
-i haven't been up to much unusual. [drawing], mostly. i installed [nixos] on both my computers and it's going pretty well so far [(less than a week)]{.note}, but every computer toucher does that at some point, so, whatever.
-
-[drawing]: https://gallery.niss.website
-[nixos]: https://nixos.org
-
-anyway, to the point.
-
-:::banner
-[go here if you just want to play with the thing][thing]
-
-:::
-
-# the point {.unnumbered}
-
-the animal-inclined might know that [q.t.][qt] can change its colour any time it wants. if you click that link you can clearly see i have some tendencies, but it can in theory be anything. so something i have wanted for a while is a page where you can click a button and get a bespoke randomly-generated quox theme of your very own.
-
-so i did that.
-
-:::aside
-you can also skip to [what i _actually_ ended up doing](#actual), if you don't care about the false starts.
-:::
-
-[qt]: https://gallery.niss.website/by-any/#qt
-
-# doing that
-
-{.floating .expandable .nobg .shaped}
-
-pretty much what i want to do, at least to begin with, is take the original colours of the image and move the hues around at random.
-
-if you look at [mdn], you might see this interesting [`hue-rotate()`][hr] thing that might do what i want. let's have a look.
-
-[mdn]: https://developer.mozilla.org/en-US/docs/Web/CSS
-[hr]: https://developer.mozilla.org/en-US/docs/Web/CSS/filter-function/hue-rotate
-
-> **Note:** `hue-rotate()` is specified as a matrix operation on the RGB color. It does not actually convert the color to the HSL model, which is a non-linear operation. Therefore, it may not preserve the saturation or lightness of the original color, especially for saturated colors.
-
-well that doesn't sound very promising. but maybe it'll be fine, so let's try it. first, separate the pictures from [q.t.'s refsheet][ref] into bits. like this.
-
-[ref]: https://gallery.niss.website/main/niss/2024-06-27-qt
-
-{.expandable .lightbg}
-
-now let's layer them back on top of each other with some css.
-
-```html
-
-
-
-
-
-
-
-
-```
-
-{.floating .left .nobg .expandable .shaped}
-
-ok, next, actually try to do the hue stuff. to check it works at all, i shoved everything to hue 0° (using krita's _hue HSL_ blend mode), and used `hue-rotate()` to change it back to the 'main' colour of each region---it won't look exact, but it'll be close.
-
-```css
-#container img { filter: hue-rotate(var(--hue)); }
-
-#outer { --hue: 273deg; } #belly { --hue: 26deg; }
-#eyes { --hue: 133deg; } #masks { --hue: 284deg; }
-#stripes { --hue: 188deg; } #lines { --hue: 273deg; }
-/* also add the id to each image */
-```
-
-right?
-
-{.expandable .nobg}
-
-well that's no good at all. i guess that warning was serious.
-
-# ok what about blend modes
-
-{.floating .expandable}
-
-all right, fine. what else. as a chronic over-user of `overlay`, i can certainly tell you that css has a few [blending modes][bm]. not as many as krita, which has approximately "too many", but enough for most purposes. one of them is `hue`. how about that.
-
-[bm]: https://developer.mozilla.org/en-US/docs/Web/CSS/blend-mode
-
-this takes a bit more messing, because i need to create a flood fill of one of the colours from that layer, and blend with that. so how about an SVG filter, i guess. or, six SVG filters---one for each filter, since you can't parametrise them.
-
-time to copy and paste the same five lines six times. yaaaaaaaaay
-
-{.bigemoji .pixel} \
-
-```svg
-
-```
-
-```css
-#outer { filter: url(#fouter); }
-/* …etc… */
-```
-
-and…
-
-{.expandable .nobg}
-
-i was expecting at least the same thing, but a different, also wrong, result is pretty cool.
-
-# drastic measures {#actual}
-
-ok, enough messing around, time to bite the bullet. separate every single colour into its own layer, and use those as _masks_ for colour fills.
-
-now the pieces look like _this_:
-
-{.expandable .lightbg}
-
-the colours in the images no longer matters, only the alpha channel. [(except for the eyes.)]{.note} each one is just a mask over a background fill of the right colour.
-
-```css
-@layer {
- #container { position: relative; width: 90vw; aspect-ratio: 3439/2240; }
- #container div { position: absolute; inset: 0; mask-size: contain; }
-}
-
-@layer {
- #static { background: url(front/static.png) 0 0 / contain; }
- #eye-shine {
- background: url(front/eyes.png) 0 0 / contain;
- mix-blend-mode: luminosity;
- }
- /* the others all look like this: */
- #spines {
- background: oklch(30.77% 0.1306 var(--hue)); --hue: 298.19;
- mask-image: url(front/spines.png);
- }
- /* etc… */
-}
-```
-
-```html
-
-
-
-
-
-
-
-
-```
-
-since the hue is separated out into a variable, i can just do:
-
-```js
-for (const elem of document.getElementsByClassName('part')) {
- elem.style.setProperty('--hue', Math.random() * 360);
-}
-```
-
-and instantly i have _something_ working. i used `oklch` because it was more likely than `hsl` or whatever to keep the colours the same kind of distance from each other, since that is what it's designed for.
-
-{.expandable .hasborder}
-
-
-# keeping the colours in sync
-
-so as of last year, most browsers got a thing called [relative colours]. if you have an existing colour `--hi`, you can rotate its hue by half a turn by saying something like
-
-[relative colours]: https://developer.mozilla.org/en-US/docs/Web/CSS/CSS_colors/Relative_colors
-
-```css
-:root {
- --hi: #ea9aa1;
- --wow: oklch(from var(--hi) l c calc(h + 180));
-}
-```
-
----
-header-includes: |
-
-...
-
-
-
\--hi
-
\--wow
-
-
-you're taking the value of `var(--hi)`, keeping the lightness and chroma channels the same, and adding 180° to the hue.
-
-:::aside
-that's not quite true. safari, as always, does it slightly wrong. according to the spec, all channels in a relative colour must be dimensionless, but in safari, the hue is an ``. other browsers, following the spec correctly, _don't allow_ that. so you _actually_ have to write
-
-```css
-:root {
- --hi: #ea9aa1;
- --wow: oklch(from var(--hi) l c calc(h + 180));
-}
-@supports (color: oklch(from red l c 10deg)) {
- :root { --wow: oklch(from var(--hi) l c calc(h + 180deg)); }
-}
-```
-
-thanks apple!
-:::
-
-so based on that, i can pick one initial colour and base all the others on it. like
-
-```css
-:root {
- /* these aren't attempting to be the same colours, just guessing something
- that MIGHT look nice */
- --outer: #57267e;
- --spines: oklch(from var(--outer) calc(l * .75) calc(c * 1.25) h);
- --vitiligo1: oklch(from var(--outer) calc(1 - (1 - l)/4) calc(c / 2) h);
-
- /* static l/c values because the socks are always some pale colour */
- --stripes: oklch(from var(--outer) .9 12.5% calc(h + 120));
- --cuffs: oklch(from var(--stripes) .8 25% h);
- /* etc */
-}
-
-.outer { background: var(--outer); mask-image: url(front/outer.png); }
-/* etc */
-```
-
-so after guessing a bunch of relative colours, i ended up with this:
-
-{.expandable .nobg}
-
-
-## notes for niss. if this goes online i fucked up
-
-- palette types
-- randomise distance between analogous colours
-- light, dark, light-dark, dark-light (belly vs outer)
-- reinstate chaos mode
-- can you set the random seed in the browser
- - no. anyway the algorithm might be different
- - make yr own
- - or . whatever
-- if so: use that to make palette permalinks
diff --git a/posts-wip/rainbow-quox/blends.avif b/posts-wip/rainbow-quox/blends.avif
deleted file mode 100644
index e6904bc..0000000
Binary files a/posts-wip/rainbow-quox/blends.avif and /dev/null differ
diff --git a/posts-wip/rainbow-quox/dark.avif b/posts-wip/rainbow-quox/dark.avif
deleted file mode 100644
index c75851f..0000000
Binary files a/posts-wip/rainbow-quox/dark.avif and /dev/null differ
diff --git a/posts-wip/rainbow-quox/dark2.avif b/posts-wip/rainbow-quox/dark2.avif
deleted file mode 100644
index 58be28b..0000000
Binary files a/posts-wip/rainbow-quox/dark2.avif and /dev/null differ
diff --git a/posts-wip/rainbow-quox/pieces1.avif b/posts-wip/rainbow-quox/pieces1.avif
deleted file mode 100644
index dcad189..0000000
Binary files a/posts-wip/rainbow-quox/pieces1.avif and /dev/null differ
diff --git a/posts-wip/rainbow-quox/pieces2.avif b/posts-wip/rainbow-quox/pieces2.avif
deleted file mode 100644
index 4b3e60a..0000000
Binary files a/posts-wip/rainbow-quox/pieces2.avif and /dev/null differ
diff --git a/posts-wip/rainbow-quox/quoxes1.avif b/posts-wip/rainbow-quox/quoxes1.avif
deleted file mode 100644
index 3060729..0000000
Binary files a/posts-wip/rainbow-quox/quoxes1.avif and /dev/null differ
diff --git a/posts/aoc2024.md b/posts/aoc2024.md
new file mode 100644
index 0000000..d3cc8bd
--- /dev/null
+++ b/posts/aoc2024.md
@@ -0,0 +1,191 @@
+---
+title: advent of code 2024, day 1, part 1
+date: 2024-12-02
+tags: [computer, quox. the language, december adventure]
+summary: don't expect me to do the whole thing okay
+...
+
+i don't think i'm going to __get into it__ this year. maybe this will be the only one i do. but i did this one.
+
+i haven't done much on quox this year [(nothing in the last… six months…)]{.note}, but it's not abandoned! i promise.
+
+it even has the beginnings of a standard library! which also mostly existed last year too.
+
+```quox
+load "bool.quox"
+load "ordering.quox"
+load "list.quox"
+load "nat.quox"
+load "string.quox"
+load "io.quox"
+```
+
+it's not very big, though, so it doesn't have line splitting yet. that's fine though.
+
+```quox
+def lines : ω.String → List String =
+ λ str ⇒ string.split (char.eq char.newline) str
+```
+
+:::aside
+**what does ω mean?**
+quox has linear types, which means that by default, each argument to a function, both sites of a pair, etc., have to be used exactly once in each code path. for function arguments that need to be uses more flexibly than that (more than once, a statically-unknown number of times, or whatever), they can be marked `ω` like above. the function passed to `string.split` also has the type `ω.Char → Bool`. it wouldn't be very useful if testing a character also consumed it: then you wouldn't be able to put it in the string.
+
+obviously this is not a very _ergonomic_ design. at some point i want to have something that fills the same role as rust's borrowed values, but that is not yet the case. so right now there are _lots_ of `ω`s.
+:::
+
+
+so. let's actually read [the puzzle][aoc1]. blah blah blah… elves… lists of numbers… blah blah… right.
+
+- list of pairs of numbers
+- [(read the string representation into actual numbers)]{.note}
+- unzip the pairs into two lists of numbers
+- sort each list
+- find the difference between each corresponding element in the sorted lists and sum them
+
+[aoc1]: https://adventofcode.com/2024/day/1
+
+:::{.aside .floating .right}
+one of the bits of detritus in the growing stdlib is half an implementation of merge sort. the half that's possible.
+:::
+
+easy, except, oh no. __sorting__. that's not very structurally recursive. [(reminder: the only recursion is natural numbers)]{.note}
+
+after thinking about whether i can model [`@accessibility predicates@`][acc] with what i already have for an hour---i don't think so---i decided to just give up and use insertion sort. that's structurally recursive. the list isn't gonna be _that_ long.
+
+[acc]: https://github.com/agda/agda-stdlib/blob/master/src/Induction/WellFounded.agda#L40-L43
+
+
+currently, the way lists are defined is via `@vectors@`, which are what people with dependent type brain call lists of known length. not arrays. sorry it's not my fault. we get vectors by recursion on our one recursive thing.
+
+```quox
+def0 Vec : ℕ → Type → Type =
+ λ len A ⇒
+ case len return Type of {
+ zero ⇒ {nil};
+ succ len', Tail ⇒ A × Tail
+ };
+```
+
+:::{.figure .floating .right .shaped .nobg}
+
+:::
+
+in a match on a `ℕ`, there is (optionally) a second variable in the `succ` case, which is the result of a recursive call. in this case, in a call to `Vec 4 ℕ`, `Tail` refers to the result of `Vec 3 ℕ` (which is `ℕ × ℕ × ℕ × {nil}`).
+
+types that look `\{like, this}` are enums. values of an enum type look like `'this`.
+
+finally, a `List A` is just a number, paired with a vector of that length.
+
+```quox
+def0 List : Type → Type = (len : ℕ) × Vec len A
+```
+
+given a definition of a comparison function, it's possible to insert a value into a vector of length `n`, getting one of length `succ n` in return. apart from the excessive annotations (also not done yet: any kind of anything-inference!) and the slightly weird-looking recursive call, this should be pretty normal.
+
+```quox
+def0 Ordering : Type = {lt, eq, gt}
+def0 Compare : Type → Type = λ A → ω.A → ω.A → Ordering
+
+def insertV :
+ 0.(A : Type) → ω.(Compare A) → ω.(len : ℕ) →
+ ω.A → ω.(Vec len A) → Vec (succ len) A =
+ λ A cmp len ⇒
+ caseω len return len' ⇒ ω.A → ω.(Vec len' A) → Vec (succ len') A of {
+ zero ⇒ λ x _ ⇒ (x, 'nil);
+ succ len', ω.inTail ⇒ λ x xs ⇒
+ let0 len : ℕ = succ len'; Res : Type = Vec (succ len) A in
+ caseω xs return Res of { (y, ys) ⇒
+ case cmp x y return Res of {
+ 'lt ⇒ (x, y, ys);
+ 'eq ⇒ (x, y, ys);
+ 'gt ⇒ (y, inTail x ys)
+ }
+ }
+ }
+```
+
+if you strip away those bits, you essentially get the equivalent of this.
+
+```haskell
+insertV :: (α → α → Ordering) → α → [α] → [α]
+insertV cmp x [] = [x]
+insertV cmp x (y:ys) = case cmp x y of
+ LT → x : y : ys
+ EQ → x : y : ys
+ GT → y : insertV cmp x ys
+```
+
+to insert into a list, just take the length off and put the new one back on.
+
+```quox
+def insert : 0.(A : Type) → ω.(Compare A) → ω.A → ω.(List A) → List A =
+ λ A cmp x ys ⇒
+ letω len = fst ys; elems = snd ys in
+ (succ len, insertV A cmp len x elems)
+```
+
+so to inefficiently sort a list, take each element, one by one, and insert it into the right place!
+
+```quox
+def sort : 0.(A : Type) → ω.(Compare A) → ω.(List A) → List A =
+ λ A cmp ⇒ list.foldrω A (List A) (list.Nil A) (insert A cmp)
+```
+
+does it work? let's write one (1) test. \
+if it doesn't, then `sort ℕ (λ m n ⇒ nat.compare m n) (5, 1,4,2,5,3,'nil)` (probably) won't reduce to the right thing, and the definition won't typecheck.
+
+```quox
+def0 sort-14253 :
+ sort ℕ (λ m n ⇒ nat.compare m n) (5, 1,4,2,5,3,'nil)
+ ≡ (5, 1,2,3,4,5,'nil) : List ℕ =
+ δ _ ⇒ (5, 1,2,3,4,5,'nil)
+```
+
+good enough for me!
+
+next up, symmetric difference. or `|x - y|`, or whatever you wanna call it. you can do that by recursing on both arguments in lockstep, which luckily is something i added to the stdlib last year. oh and in the compiled output just use scheme's arithmetic operators instead of going O(n).
+
+```quox
+#[compile-scheme "(lambda% (m n) (abs (- m n)))"]
+def sd : ω.ℕ → ω.ℕ → ℕ =
+ nat.elim-pairω (λ _ _ ⇒ ℕ)
+ 0 -- |0 - 0| = 0
+ (λ m _ ⇒ succ m) -- |succ m - 0| = succ m
+ (λ n _ ⇒ succ n) -- |0 - succ n| = succ n
+ (λ _ _ d ⇒ d) -- |succ m - succ n| = |m - n|
+
+def0 sd-6-3 : sd 6 3 ≡ 3 : ℕ = δ _ ⇒ 3
+def0 sd-3-6 : sd 3 6 ≡ 3 : ℕ = δ _ ⇒ 3
+```
+
+now the annoying part. chopping up lines. break it on whitespace, then on non-whitespace, and convert the first and third parts to numbers.
+
+```quox
+def number-pair : ω.String → ℕ × ℕ =
+ λ str ⇒
+ letω a_bc = string.break char.ws? str;
+ a = fst a_bc; bc = snd a_bc;
+ c = snd (string.span char.ws? bc) in
+ (string.to-ℕ-or-0 a, string.to-ℕ-or-0 c)
+```
+
+and the main function. boy i wish i had some `do` notation right now..! one day.
+
+```quox
+#[main]
+def part1 : IO True =
+ io.bindω String True (io.read-fileω "1.txt") (λ str ⇒
+ letω pairs = list.mapω String (ℕ × ℕ) number-pair (lines str);
+ lists = list.unzip ℕ ℕ pairs;
+ sortℕ = sort ℕ (λ m n ⇒ nat.compare m n);
+ as = sortℕ (fst lists); bs = sortℕ (snd lists);
+ diffs = list.zip-with-uneven ℕ ℕ ℕ sd as bs;
+ in
+ io.dump ℕ (list.sum diffs))
+```
+
+after taking almost four entire seconds to compile, it… works. after i add another `compile-scheme` thing to the stdlib's `nat.compare`, anyway.
+
+i had other things to do today so i didn't get around to even looking at part two.
+bye []{.emojiseq}
diff --git a/posts/aoc2024/succ.png b/posts/aoc2024/succ.png
new file mode 100644
index 0000000..b389e64
Binary files /dev/null and b/posts/aoc2024/succ.png differ
diff --git a/posts/rainbow-quox.md b/posts/rainbow-quox.md
new file mode 100644
index 0000000..e71b0bc
--- /dev/null
+++ b/posts/rainbow-quox.md
@@ -0,0 +1,216 @@
+---
+title: rainbow quox
+date: 2024-12-03
+tags: [computer, website, fursona, december adventure]
+summary: q.t. colour scheme generator
+header-includes: |
+
+...
+
+the animal-inclined might know that [q.t.][qt] can change its colour any time it wants. if you click that link you can clearly see i have some tendencies, but it can in theory be anything. so something i have wanted for a while is a page where you can click a button and get a bespoke randomly-generated quox theme of your very own.
+
+so for today's [`@december adventure@`][decadv], i did that. (yesterday's was retroactively the AOC stuff.)
+
+[decadv]: https://eli.li/december-adventure
+
+:::banner
+[go here if you just want to play with the thing][thing]
+:::
+
+[thing]: https://yummy.cricket/rainbow-quox
+
+you can also skip to [what i _actually_ ended up doing](#actual), if you don't care about the false starts.
+
+[qt]: https://gallery.niss.website/by-any/#qt
+
+# doing that
+
+{.floating .expandable .nobg .shaped}
+
+pretty much what i want to do, at least to begin with, is take the original colours of the image and move the hues around at random.
+
+if you look at [mdn], you might see this interesting [`hue-rotate()`][hr] thing that might do what i want. let's have a look.
+
+[mdn]: https://developer.mozilla.org/en-US/docs/Web/CSS
+[hr]: https://developer.mozilla.org/en-US/docs/Web/CSS/filter-function/hue-rotate
+
+> **Note:** `hue-rotate()` is specified as a matrix operation on the RGB color. It does not actually convert the color to the HSL model, which is a non-linear operation. Therefore, it may not preserve the saturation or lightness of the original color, especially for saturated colors.
+
+
+{.floating .right .nobg .expandable .shaped}
+
+well that doesn't sound very encouraging. but maybe it'll be fine.
+
+i shoved [all of the colours][jofo] to hue 0° (using krita's _hue HSL_ blend mode), and used `hue-rotate()` to change it back to the 'main' colour of each region.
+
+it won't look exact, but it'll be close. right?
+
+[jofo]: https://johnnyforeigner.bandcamp.com/track/all-of-the-colours
+
+{.expandable .nobg}
+
+well that's no good at all. i guess that warning was serious.
+
+# ok what about blend modes
+
+all right, fine. what else. as a chronic over-user of `overlay`, i can certainly tell you that css has a few [blending modes][bm]. not as many as krita, which has approximately "too many", but enough for most purposes. one of them is `hue`. how about that.
+
+[bm]: https://developer.mozilla.org/en-US/docs/Web/CSS/blend-mode
+
+this takes a bit more messing, because i need to create a flood fill of one of the colours from that layer, and blend with that. so how about an SVG filter, i guess. or, six SVG filters---one for each layer, since you can't parametrise them. each one looks like this, with a different `flood-color`.
+
+```svg
+
+
+
+
+
+```
+
+and…
+
+{.expandable .nobg}
+
+i was expecting at least the same thing, but a different, also wrong, result is pretty cool.
+
+# drastic measures {#actual}
+
+ok, enough messing around, time to bite the bullet. separate _every_ colour into its own layer, and use those as masks for colour fills.
+
+```css
+#spines {
+ background: oklch(30.77% 0.1306 var(--hue)); --hue: 298.19;
+ mask-image: url(front/spines.png);
+}
+/* etc… */
+```
+
+since the hue is separated out into a variable, i can just randomise them all and instantly have _something_ working.
+
+{.expandable .hasborder #chaos}
+
+
+# digression about relative colours
+
+[» skip »](#js)
+
+another thing i played with was using [`@relative colours@`][relcol] to generate a whole palette from one starting colour. relative colours work like this: if you have an existing colour `--hi`, you can rotate its hue by half a turn (in real `oklch` this time!!!), keeping its luma and chroma the same, by saying this:
+
+```css
+:root {
+ --hi: #ea9aa1;
+ --wow: oklch(from var(--hi) l c calc(h + 180));
+}
+```
+
+
+
\--hi
+
\--wow
+
+
+[relcol]: https://developer.mozilla.org/en-US/docs/Web/CSS/CSS_colors/Relative_colors
+
+so i tried that. after guessing a bunch of relative colours, i ended up with this:
+
+{.expandable .nobg}
+
+
+# just do it in ~~java~~typescript. fine {#js}
+
+that was pretty cool, but i decided i actually want more flexibility. lighter and darker colour schemes. triadic schemes. whatever.
+
+maybe that would be possible in pure css with increasingly illegible relative colours. but the randomise button is going to need javascript anyway, so i might as well just fill in the colours directly. but `oklch` is still useful for generating consistent palettes.
+
+the constraints for a "good" q.t. are something like:
+
+1. the spines should be a similar colour to its main body.
+2. the same applies to the four fin colours; the belly colours; the sock colours; and the mask and claw colours.
+3. the belly should be very different from the rest of the body.
+4. the eyes should be a similar colour to the body, the fins, or the belly.
+5. the vitiligo patches should match the colour that they are on.
+6. the sock stripes should be pale and not too saturated.
+
+a good place to start is the same place everyone does: with complementary and triadic colours.
+
+:::{#patterns}
+{.expandable .nobg}
+
+{.expandable .nobg}
+
+{.expandable .nobg}
+:::
+
+using this as a starting point, i pick some evenly-spaced colours for each bit. the final palettes come out like this!
+
+:::{#result}
+- fins:
+
+- body:
+
+- belly:
+
+- mask/claws/socks:
+
+
+{ .right .expandable .nobg}
+:::
+
+# ok what now
+
+it's not finished. some things i plan to add at, uh, some point, include:
+
+- put [chaos mode](#chaos) back in.
+- permalinks for colour schemes. to do this i need to write another random number generator, since `Math.random` can't be manually seeded. and by "write" i mean "look up online".
+- colour schemes with a light body and dark belly, rather than the other way around.
+- render onto a `
- 
- 
-
+:::
+
+in a match on a `ℕ`, there is (optionally) a second variable in the `succ` case, which is the result of a recursive call. in this case, in a call to `Vec 4 ℕ`, `Tail` refers to the result of `Vec 3 ℕ` (which is `ℕ × ℕ × ℕ × {nil}`).
+
+types that look `\{like, this}` are enums. values of an enum type look like `'this`.
+
+finally, a `List A` is just a number, paired with a vector of that length.
+
+```quox
+def0 List : Type → Type = (len : ℕ) × Vec len A
+```
+
+given a definition of a comparison function, it's possible to insert a value into a vector of length `n`, getting one of length `succ n` in return. apart from the excessive annotations (also not done yet: any kind of anything-inference!) and the slightly weird-looking recursive call, this should be pretty normal.
+
+```quox
+def0 Ordering : Type = {lt, eq, gt}
+def0 Compare : Type → Type = λ A → ω.A → ω.A → Ordering
+
+def insertV :
+ 0.(A : Type) → ω.(Compare A) → ω.(len : ℕ) →
+ ω.A → ω.(Vec len A) → Vec (succ len) A =
+ λ A cmp len ⇒
+ caseω len return len' ⇒ ω.A → ω.(Vec len' A) → Vec (succ len') A of {
+ zero ⇒ λ x _ ⇒ (x, 'nil);
+ succ len', ω.inTail ⇒ λ x xs ⇒
+ let0 len : ℕ = succ len'; Res : Type = Vec (succ len) A in
+ caseω xs return Res of { (y, ys) ⇒
+ case cmp x y return Res of {
+ 'lt ⇒ (x, y, ys);
+ 'eq ⇒ (x, y, ys);
+ 'gt ⇒ (y, inTail x ys)
+ }
+ }
+ }
+```
+
+if you strip away those bits, you essentially get the equivalent of this.
+
+```haskell
+insertV :: (α → α → Ordering) → α → [α] → [α]
+insertV cmp x [] = [x]
+insertV cmp x (y:ys) = case cmp x y of
+ LT → x : y : ys
+ EQ → x : y : ys
+ GT → y : insertV cmp x ys
+```
+
+to insert into a list, just take the length off and put the new one back on.
+
+```quox
+def insert : 0.(A : Type) → ω.(Compare A) → ω.A → ω.(List A) → List A =
+ λ A cmp x ys ⇒
+ letω len = fst ys; elems = snd ys in
+ (succ len, insertV A cmp len x elems)
+```
+
+so to inefficiently sort a list, take each element, one by one, and insert it into the right place!
+
+```quox
+def sort : 0.(A : Type) → ω.(Compare A) → ω.(List A) → List A =
+ λ A cmp ⇒ list.foldrω A (List A) (list.Nil A) (insert A cmp)
+```
+
+does it work? let's write one (1) test. \
+if it doesn't, then `sort ℕ (λ m n ⇒ nat.compare m n) (5, 1,4,2,5,3,'nil)` (probably) won't reduce to the right thing, and the definition won't typecheck.
+
+```quox
+def0 sort-14253 :
+ sort ℕ (λ m n ⇒ nat.compare m n) (5, 1,4,2,5,3,'nil)
+ ≡ (5, 1,2,3,4,5,'nil) : List ℕ =
+ δ _ ⇒ (5, 1,2,3,4,5,'nil)
+```
+
+good enough for me!
+
+next up, symmetric difference. or `|x - y|`, or whatever you wanna call it. you can do that by recursing on both arguments in lockstep, which luckily is something i added to the stdlib last year. oh and in the compiled output just use scheme's arithmetic operators instead of going O(n).
+
+```quox
+#[compile-scheme "(lambda% (m n) (abs (- m n)))"]
+def sd : ω.ℕ → ω.ℕ → ℕ =
+ nat.elim-pairω (λ _ _ ⇒ ℕ)
+ 0 -- |0 - 0| = 0
+ (λ m _ ⇒ succ m) -- |succ m - 0| = succ m
+ (λ n _ ⇒ succ n) -- |0 - succ n| = succ n
+ (λ _ _ d ⇒ d) -- |succ m - succ n| = |m - n|
+
+def0 sd-6-3 : sd 6 3 ≡ 3 : ℕ = δ _ ⇒ 3
+def0 sd-3-6 : sd 3 6 ≡ 3 : ℕ = δ _ ⇒ 3
+```
+
+now the annoying part. chopping up lines. break it on whitespace, then on non-whitespace, and convert the first and third parts to numbers.
+
+```quox
+def number-pair : ω.String → ℕ × ℕ =
+ λ str ⇒
+ letω a_bc = string.break char.ws? str;
+ a = fst a_bc; bc = snd a_bc;
+ c = snd (string.span char.ws? bc) in
+ (string.to-ℕ-or-0 a, string.to-ℕ-or-0 c)
+```
+
+and the main function. boy i wish i had some `do` notation right now..! one day.
+
+```quox
+#[main]
+def part1 : IO True =
+ io.bindω String True (io.read-fileω "1.txt") (λ str ⇒
+ letω pairs = list.mapω String (ℕ × ℕ) number-pair (lines str);
+ lists = list.unzip ℕ ℕ pairs;
+ sortℕ = sort ℕ (λ m n ⇒ nat.compare m n);
+ as = sortℕ (fst lists); bs = sortℕ (snd lists);
+ diffs = list.zip-with-uneven ℕ ℕ ℕ sd as bs;
+ in
+ io.dump ℕ (list.sum diffs))
+```
+
+after taking almost four entire seconds to compile, it… works. after i add another `compile-scheme` thing to the stdlib's `nat.compare`, anyway.
+
+i had other things to do today so i didn't get around to even looking at part two.
+bye [