def fin_of

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

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

47def fin_of(+bound: Nat, +value: Nat) -> Maybe<&2, Shape.Fin(bound)>:
48  match bound value:
49    case 0n value:
50      None{}
51    case 1n+p 0n:
52      Some{Shape.FZero{}}
53    case 1n+p 1n+q:
54      fin_of.next(p, fin_of(p, q))