def split_shift

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

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

24def split_shift(+a: Nat, +b: Nat, +index: Shape.Fin(b)) -> {Shape.Fin.split(a, b, Shape.Fin.shift(a, b, index)) == Inr{index} : Either<Shape.Fin(a), Shape.Fin(b)>}:
25  match a:
26    case 0n:
27      {==}
28    case 1n+p:
29      %split_shift(p, b, index) : {Shape.Fin.split.step(p, b, Shape.Fin.split(p, b, Shape.Fin.shift(p, b, index))) == Shape.Fin.split.step(p, b, _) : Either<Shape.Fin(1n+p), Shape.Fin(b)>}
30      {==}