def decb

lawful-fields@0.1.1.0 · defs.bend:80

import Base

80# A decimal number below bound; None otherwise. The laws use bound = 2^32 (what
81# fits a U32), written Nat.pow(2n, 32n) in each law: the checker evaluates a
82# constant hidden in a definition, and 2^32 in unary is too deep.
83def decb(xs: List<&2, U32>, +bound: Nat) -> Maybe<&2, Nat>:
84  decb.of(dec(xs), bound)