def e8

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes.bend as Bytes

import Base

84# 8 n
85def e8(n: Nat) -> Nat:
86  match n:
87    case 0n:
88      0n
89    case 1n+k:
90      Nat.add(8n, e8(k))

Uses (2)