def mb

lawful-bytes@0.1.1.0 · proof_core.bend:34

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

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