factorial — 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 factorial.lean prints nothing when every receipt passes

import Room
open Room
set_option autoImplicit false

#guard (perms [1, 2, 3]).length == 6
#guard fact 4 == 24
#guard (perms [1, 2, 3, 4]).length == 24
#guard (inserts 0 [1, 2]).length == 3
#guard joinMap (inserts 0) [[1], [2]] == [[0, 1], [1, 0], [0, 2], [2, 0]]

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