candidate i's entry of a column of eight
531def coppeliusTiledPick = (lambda unrestricted i : Nat .
532 (lambda unrestricted v0 : Nat . (lambda unrestricted v1 : Nat . (lambda unrestricted v2 : Nat . (lambda unrestricted v3 : Nat .
533 (lambda unrestricted v4 : Nat . (lambda unrestricted v5 : Nat . (lambda unrestricted v6 : Nat . (lambda unrestricted v7 : Nat .
534 (naturalSelect (naturalEqual i 0) v0 (naturalSelect (naturalEqual i 1) v1 (naturalSelect (naturalEqual i 2) v2
535 (naturalSelect (naturalEqual i 3) v3 (naturalSelect (naturalEqual i 4) v4 (naturalSelect (naturalEqual i 5) v5
536 (naturalSelect (naturalEqual i 6) v6 v7))))))))))))))))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.