law list_len
import lawful-fields@0.1.1.0/proof_digits.bend as ProofDigitsimport 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}
import lawful-fields@0.1.1.0/proof_digits.bend as ProofDigitsimport 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}