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

import Room
open Room
set_option autoImplicit false

#guard val [true, false, true] == 5
#guard val (again inc 5 (zeros 3)) == 5
#guard again inc 8 (zeros 3) == zeros 3
#guard dec (inc [true, true, false]) == [true, true, false]
#guard val (clockAt 3 5) == 5

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