def rep

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/consts.bend:39

import Base

39# n copies of k, then tl
40def rep(n: Nat, +k: U32, tl: List<&2, U32>) -> List<&2, U32>:
41  match n:
42    case 0n:
43      tl
44    case 1n+m:
45      Con{k, rep(m, k, tl)}