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

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

import Face
open Room Face
set_option autoImplicit false

#guard [true, false].all (fun x => [true, false].all (fun y => [true, false].all
  (fun z => (x == y) || (y == z) || (x == z))))
#guard census 3 == 2
#guard census 4 == 5
#guard (walkIn (fun a b : Nat => a + b)
  ((pairFace (appFace Unit Nat) (appFace Unit Nat) (fun n : Nat => fun _ => n)
    (fun n : Nat => fun _ => n + n)).obs (7 : Nat) (atTheDoor () ())) == 21)

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