ProofCore.mb: def of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/proof_core.bend as ProofCore
Lines 34-40 of lawful-bytes@0.1.1.0/proof_core.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&start_line=34&end_line=40

import Base
import lawful-words@0.1.0.0/defs.bend as W

# What a Maybe word gives for byte r.
def mb(m: Maybe<&2, U32>, +r: Nat) -> Maybe<&2, U32>:
  match m:
    case None{}:
      None{}
    case Some{w}:
      Some{W.byte(w, r)}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/defs.bend&name=byte