def le_all

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/value.bend:29

import Base

29def le_all(xs: List<&2, U32>, +b: Nat) -> Bool:
30  match xs:
31    case Nil{}: True{}
32    case x <> t: Bool.and(Nat.is_le(v(x), b), le_all(t, b))