every product Coppelius launches has a recorded choice, and it serves the
product (decided before any program is built)
644def coppeliusTiledChoicesAdmitted : Nat =
645 (eliminate StdList (lambda unrestricted c : (family StdList (family CoppeliusTiledShape)) . Nat) coppeliusTiledShapes
646 (branch StdListEmpty . 1)
647 (branch StdListCons head tail induction .
648 (naturalAnd induction
649 (eliminate CoppeliusTiledShape (lambda unrestricted c : (family CoppeliusTiledShape) . Nat) head
650 (branch CoppeliusTiledShapeValue a b m n k residual .
651 (naturalAnd (naturalLess (coppeliusTiledChoiceFor residual a b m n k) coppeliusTiledCandidateCount)
652 (coppeliusTiledTileServes (coppeliusTiledTile residual a b m n k) m n k)))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.