def nth_v

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
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/point.bend as P

61def nth_v(+one: Nat, +h1: {one == 1n : Nat}, i: Nat, rs: List<&2, List<&2, Nat>>) -> {FS.value(one, P.nth(i, rs)) == CV.nth(i, vals(one, rs)) : Nat}:
62  match i rs:
63    case 0n Nil{}:
64      zero_v(one, h1)
65    case 1n+k Nil{}:
66      zero_v(one, h1)
67    case 0n r <> t:
68      {==}
69    case 1n+ +k r <> +t:
70      nth_v(one, h1, k, t)