def len_le

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

import Base

24def len_le(n: Nat, xs: List<&2, U32>) -> Bool:
25  match n:
26    case 0n:
27      match xs:
28        case Nil{}:
29          True{}
30        case Con{x, xt}:
31          False{}
32    case 1n+m:
33      match xs:
34        case Nil{}:
35          True{}
36        case Con{x, xt}:
37          len_le(m, xt)