def rs.empty

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1732

import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M

1732def rs.empty(+e: M.CmError, +u: Unit, h: {Fail{e} == Done{u} : Result<&2, &2, M.CmError, Unit>}) -> Empty:
1733  %h : rs.disc(_)
1734  Unit{}