Core.Fin.unpack.step: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/core.bend as Core
Lines 116-121 of bendtorch-core@0.1.0.0/src/shape/core.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&start_line=116&end_line=121

import Base

def Fin.unpack.step(-a: Nat, -b: Nat, rec: Fin(Nat.mul(a, b)) -> Fin(a) & Fin(b), split: Either<Fin(b), Fin(Nat.mul(a, b))>) -> Fin(1n+a) & Fin(b):
  match split:
    case Inl{tail}:
      (FZero{}, tail)
    case Inr{index}:
      Fin.unpack.lift(a, b, rec(index))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Either
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.unpack.lift