Coppelius.Build.TiledChoices · Source

def · lines 19–38
coppeliusTiledChoice

residual, A as columns, B as columns, m, n, k -> the candidate
19def coppeliusTiledChoice = (lambda unrestricted residual : Nat . (lambda unrestricted aColumns : Nat .
20  (lambda unrestricted bColumns : Nat . (lambda unrestricted m : Nat . (lambda unrestricted n : Nat .
21  (lambda unrestricted k : Nat .
22    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 0) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 1536) (naturalEqual k 512)))))) 1
23    (naturalSelect (naturalAnd (naturalEqual residual 1) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 0) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 512) (naturalEqual k 512)))))) 3
24    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 0) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 1408) (naturalEqual k 512)))))) 3
25    (naturalSelect (naturalAnd (naturalEqual residual 1) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 0) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 512) (naturalEqual k 1408)))))) 3
26    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 0) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 12288) (naturalEqual k 512)))))) 2
27    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 512) (naturalEqual k 1536)))))) 3
28    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 512) (naturalEqual k 512)))))) 3
29    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 512) (naturalEqual k 1408)))))) 3
30    (naturalSelect (naturalAnd (naturalEqual residual 1) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 512) (naturalEqual k 1408)))))) 3
31    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 1408) (naturalEqual k 512)))))) 1
32    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 512) (naturalEqual k 12288)))))) 2
33    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 1) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1536) (naturalAnd (naturalEqual n 512) (naturalEqual k 1024)))))) 1
34    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 1) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 512) (naturalAnd (naturalEqual n 512) (naturalEqual k 1024)))))) 2
35    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 1) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1408) (naturalAnd (naturalEqual n 512) (naturalEqual k 1024)))))) 1
36    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 1) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 512) (naturalAnd (naturalEqual n 1408) (naturalEqual k 1024)))))) 1
37    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 1) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 12288) (naturalAnd (naturalEqual n 512) (naturalEqual k 1024)))))) 3
38coppeliusTiledChoiceNone))))))))))))))))))))))
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.