def gea

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/fieldops.bend:28

import Base

28# every limb at least b
29def gea(xs: List<&2, U32>, +b: Nat) -> Bool:
30  match xs:
31    case Nil{}:
32      True{}
33    case Con{x, xt}:
34      Bool.and(Nat.is_le(b, U32.to_nat(x)), gea(xt, b))