1448def bytesDropLeadingZeroes =
1449 (lambda unrestricted value : Bytes .
1450 (bytes-eliminate
1451 (lambda unrestricted current : Bytes . Bytes)
1452 b""
1453 (lambda unrestricted head : Byte .
1454 (lambda unrestricted tail : Bytes .
1455 (lambda unrestricted induction : Bytes .
1456 (nat-eliminate
1457 (lambda unrestricted headValue : Nat . Bytes)
1458 induction
1459 (lambda unrestricted predecessor : Nat .
1460 (lambda unrestricted keepInduction : Bytes . (bytes-cons head tail)))
1461 (byte-to-nat head)))))
1462 value))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.