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

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

import Face
open Room Face
set_option autoImplicit false

def toy : Face := appFace Nat Nat
def theModel : door toy.State Nat := atTheDoor (fun n => n + 1) 3
def theOtherModel : door toy.State Nat := atTheDoor (fun n => n + 1) 99
def readAtTwo : Nat := face ((concordFace toy Nat).obs theModel (atTheDoor (2 : Nat) ()))
def modelAtTwo : Nat := met ((concordFace toy Nat).obs theModel (atTheDoor (2 : Nat) ()))
def soundMine : List Nat := sound (host toy Nat) theModel (recite ([1, 2] : List Nat))
def soundYours : List Nat := sound (host toy Nat) theOtherModel (recite ([1, 2] : List Nat))
def agreesOver (ps : List Nat) : Bool :=
  ps.all (fun p => Nat.beq (toy.obs (face theModel) p) (met theModel))

#guard readAtTwo == 3
#guard modelAtTwo == 3
#guard soundMine == soundYours
#guard soundMine == [2, 3]
#guard agreesOver [2]
#guard !(agreesOver [2, 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