def lea

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/limbs.bend:57

import Base

57# every limb at most b
58def lea(xs: List<&2, U32>, +b: Nat) -> Bool:
59  match xs:
60    case Nil{}:
61      True{}
62    case Con{x, xt}:
63      Bool.and(Nat.is_le(U32.to_nat(x), b), lea(xt, b))