def len_ge

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/poly.bend:39

import Base

39def len_ge(n: Nat, xs: List<&2, U32>) -> Bool:
40  match n:
41    case 0n:
42      True{}
43    case 1n+m:
44      match xs:
45        case Nil{}:
46          False{}
47        case Con{x, xt}:
48          len_ge(m, xt)