def allred

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/point.bend:26

import Base

26def allred(+one: Nat, rs: List<&2, List<&2, Nat>>) -> Bool:
27  match rs:
28    case Nil{}: True{}
29    case r <> t: Bool.and(red(one, r), allred(one, t))