def run_go_r

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P

113def run_go_r(+one: Nat, +h1: {one == 1n : Nat}, prog: List<&2, P.Op>, +rs: List<&2, List<&2, Nat>>, +h: {allred(one, rs) == True{} : Bool}) -> {allred(one, P.run_go(prog, rs)) == True{} : Bool}:
114  match prog:
115    case Nil{}:
116      h
117    case +op <> +t:
118      run_go_r(one, h1, t, List.append(&2, List<&2, Nat>, rs, [P.exec(op, rs)]), allred_app(one, rs, P.exec(op, rs), h, exec_r(one, h1, op, rs, h)))