def sp.cons_blocks

bend-osdev-mode-core@0.1.0.0 · PROOF.bend:80

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

80def sp.cons_blocks(b: M.CmBlock, s: M.CmSplit) -> {M.cm.split.blocks(M.cm.split.cons(b, s)) == Con{b, M.cm.split.blocks(s)} : List<&2, M.CmBlock>}:
81  match s:
82    case M.CmSplit{bs, t}:
83      {==}