def pl
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes.bend as Bytesimport Base
54# n + m, by recursion on n
55def pl(n: Nat, +m: Nat) -> Nat:
56 match n:
57 case 0n:
58 m
59 case 1n+k:
60 1n+pl(k, m)
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes.bend as Bytesimport Base
54# n + m, by recursion on n
55def pl(n: Nat, +m: Nat) -> Nat:
56 match n:
57 case 0n:
58 m
59 case 1n+k:
60 1n+pl(k, m)