Source/Systems

Coppelius.Build.DeviceImages

systems/coppelius/src/Coppelius/Build/DeviceImages.alpha

726 lines107 declarations39.5 KiBSHA-256 aca105a01057

def · lines 568–574

coppeliusTiledName

Full file
568def coppeliusTiledName = (lambda unrestricted residual : Nat .
569  (lambda unrestricted a : (family TiledProductLayout) . (lambda unrestricted b : (family TiledProductLayout) .
570  (lambda unrestricted m : Nat . (lambda unrestricted n : Nat . (lambda unrestricted k : Nat .
571    (bytes-append b"tiled-" (bytes-append (coppeliusTiledLayoutName a) (bytes-append (coppeliusTiledLayoutName b)
572      (bytes-append b"-m" (bytes-append (naturalDecimalBytesWithin 8 m) (bytes-append b"-n" (bytes-append (naturalDecimalBytesWithin 8 n)
573        (bytes-append b"-k" (bytes-append (naturalDecimalBytesWithin 8 k)
574          (nat-eliminate (lambda unrestricted c : Nat . Bytes) b"" (lambda unrestricted p : Nat . (lambda unrestricted ignored : Bytes . b"-add")) residual))))))))))))))))

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.