law bind_cong

bend-osdev-mode-core@0.1.0.0 · LAWS.bend:157

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M

157# a bind whose continuations agree on every value agrees
158law bind_cong:
159  for r: Result<&2, &2, M.CmError, B.Octets>
160  for f: B.Octets -> Result<&2, &2, M.CmError, B.Octets>
161  for g: B.Octets -> Result<&2, &2, M.CmError, B.Octets>
162  for h: @c: B.Octets -> {f(c) == g(c) : Result<&2, &2, M.CmError, B.Octets>}
163  {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, f) == Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, g) : Result<&2, &2, M.CmError, B.Octets>}