book — a product as an assay, on Room (guards only, not grown)

0 receipts inline · 9 lines · pinned (not yet) — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean book.lean prints nothing when every receipt passes

import Room
open Room
set_option autoImplicit false

#guard (words 0).length == 1
#guard (words 1).length == 2
#guard (words 2).length == 4
#guard (words 3).length == 8
#guard (words 3).length == roomCap 3

the map of relations — every law a node, an arrow for each citation the elaborator reads (bin/counter chart; without --laws the carriers join the map)

graph LR