def Fin.unpack.step

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

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

import Base

116def 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):
117  match split:
118    case Inl{tail}:
119      (FZero{}, tail)
120    case Inr{index}:
121      Fin.unpack.lift(a, b, rec(index))

Uses (8)

Used by (3)