def run_r

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

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

151def run_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(prog, rs)) == True{} : Bool}:
152  %Equal.sym(List<&2, List<&2, Nat>>, P.run(prog, rs), P.run_go(prog, rs), run_is(prog, rs)) : {allred(one, _) == True{} : Bool}
153  run_go_r(one, h1, prog, rs, h)