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

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

import Face
open Room Face
set_option autoImplicit false

#guard peek (liftFrom tally (3 : Nat)) == 3
#guard feed (liftFrom tally (0 : Nat)) () [(), ()] == 3
#guard (liftFrom flip true [(), ()] : Bool)
#guard liftFrom tally (0 : Nat) [(), (), (), ()] == behavior tally [(), (), (), ()]

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