def pre_len

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/blist.bend:61

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg

61def pre_len(a: Nat, +b: Nat, xs: List<&2, U32>, +h: {B.has_len(Nat.add(a, b), xs) == True{} : Bool}) -> {B.has_len(a, CV.first(a, xs)) == True{} : Bool}:
62  match a xs:
63    case 0n _:
64      {==}
65    case 1n+k Nil{}:
66      Empty.absurd({B.has_len(1n+k, CV.first(1n+k, [])) == True{} : Bool}, Lg.false_true(h))
67    case 1n+k x <> t:
68      pre_len(k, b, t, h)