def merge_step

bendtorch-core@0.1.0.0 · src/shape/index_proofs.bend:32

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

32def merge_step(+a: Nat, +b: Nat, split: Either<Shape.Fin(a), Shape.Fin(b)>) -> {Shape.Fin.merge(1n+a, b, Shape.Fin.split.step(a, b, split)) == Shape.FNext{Shape.Fin.merge(a, b, split)} : Shape.Fin(1n+Nat.add(a, b))}:
33  match split:
34    case Inl{index}:
35      {==}
36    case Inr{index}:
37      {==}