def Fin.split

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

import Base

81def Fin.split(+a: Nat, +b: Nat, index: Fin(Nat.add(a, b))) -> Either<Fin(a), Fin(b)>:
82  match a:
83    case 0n:
84      Inr{index}
85    case 1n+p:
86      match index:
87        case FZero{}:
88          Inl{FZero{}}
89        case FNext{previous}:
90          Fin.split.step(p, b, Fin.split(p, b, previous))