167def coppeliusDeviceZeroBytes =
168 (lambda unrestricted count : Nat .
169 (nat-eliminate
170 (lambda unrestricted current : Nat . Bytes)
171 b""
172 (lambda unrestricted predecessor : Nat .
173 (lambda unrestricted induction : Bytes .
174 (bytes-cons (byte 0) induction)))
175 count))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.