law ol_room

lawful-bytes@0.1.1.0 · proof_grow.bend:107

import Base

107# Room for one more byte when the rest of the list still fits.
108law ol_room:
109  for +len: U32
110  for +r: Nat
111  for +m: Nat
112  for +hn: {Nat.is_le(Nat.add(U32.to_nat(len), 1n+r), m) == True{} : Bool}
113  {Nat.is_lt(U32.to_nat(len), m) == True{} : Bool}