law list_len

lawful-fields@0.1.1.0 · proof_digits.bend:721

import lawful-fields@0.1.1.0/proof_digits.bend as ProofDigits
import Base
import lawful-fields@0.1.1.0/fields.bend as FC

721law list_len:
722  for +n: U32
723  {Nat.is_le(List.length(&2, U32, FC.put_dec.list(n)), 10n) == True{} : Bool}

Uses (9)

Used by (1)