toy — a product as an assay, on Toy (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 toy.lean prints nothing when every receipt passes

import Face
import Toy
open Room Face Toy
set_option autoImplicit false

def threeTicks : Nat := behavior counter [(), (), ()]
def fromFour : Nat := park counter (4 : Nat) [()]
def twoFlips : Bool := park flipper true [(), ()]

#guard threeTicks == 3
#guard fromFour == 5
#guard twoFlips

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