the device address of the image named `identity`: where the backend
places its region, by the same fold (0, which no launch can name, when
there is none)
705def coppeliusDeviceImageAddress =
706 (lambda unrestricted identity : Bytes .
707 (app
708 (eliminate CoppeliusDeviceImages
709 (lambda unrestricted current : (family CoppeliusDeviceImages) . (pi unrestricted cursor : Nat . Nat))
710 coppeliusDeviceImages
711 (branch CoppeliusDeviceImagesEnd . (lambda unrestricted cursor : Nat . 0))
712 (branch CoppeliusDeviceImagesNext image tail induction .
713 (lambda unrestricted cursor : Nat .
714 (eliminate CoppeliusDeviceImage (lambda unrestricted current : (family CoppeliusDeviceImage) . Nat) image
715 (branch CoppeliusDeviceImageValue name program material registers blockX sharedBytes .
716 (let unrestricted offset = (naturalAdd cursor (coppeliusDevicePadding cursor)) in
717 (naturalSelect (bytes-equal name identity)
718 (naturalAdd coppeliusProgramBase offset)
719 (induction (naturalAdd offset (bytes-length material))))))))))
720 0))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.