def Fin.left

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

import Base

56def Fin.left(+a: Nat, -b: Nat, index: Fin(a)) -> Fin(Nat.add(a, b)):
57  match a:
58    case 0n:
59      match index:
60    case 1n+p:
61      match index:
62        case FZero{}:
63          FZero{}
64        case FNext{previous}:
65          FNext{Fin.left(p, b, previous)}