def P0

lawful-bytes@0.1.1.0 · proof_fast_word.bend:17

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-bytes@0.1.1.0/proof_core.bend as C

17# The place of the first zero byte of v (4 when there is none).
18def P0(+v: U32) -> Nat:
19  D.run_len(C.L4(v), 0)