def Fin.pack

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

import Base

99def Fin.pack(+a: Nat, +b: Nat, coordinate: Fin(a) & Fin(b)) -> Fin(Nat.mul(a, b)):
100  match a:
101    case 0n:
102      (head, tail) = coordinate
103      match head:
104    case 1n+p:
105      (head, tail) = coordinate
106      match head:
107        case FZero{}:
108          Fin.left(b, Nat.mul(p, b), tail)
109        case FNext{previous}:
110          Fin.shift(b, Nat.mul(p, b), Fin.pack(p, b, (previous, tail)))