isaac — a product as an assay, on Face (guards only, not grown)

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

import Face
open Room Face
set_option autoImplicit false

#guard behavior tally (List.replicate 5 ()) == 5
#guard Nat.beq (park tally (3 : Nat) (List.replicate 4 ())) 7
#guard Nat.beq (orbit tally (fun _ => ()) (0 : Nat) 6) 6
#guard (park flip true [(), ()] : Bool)
#guard drive (buffered tally) (settleHeld tally ((2 : Nat), [(), ()])) [()]
        == drive (buffered tally) ((2 : Nat), [(), ()]) [()]

#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