def fin_from

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

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

21def fin_from(+bound: Nat, +value: Nat, fits: {True{} == Nat.is_lt(value, bound) : Bool}) -> Shape.Fin(bound):
22  match bound value:
23    case 0n 0n:
24      Empty.absurd(Shape.Fin(0n), Shape.clash(fits))
25    case 0n 1n+q:
26      Empty.absurd(Shape.Fin(0n), Shape.clash(fits))
27    case 1n+p 0n:
28      Shape.FZero{}
29    case 1n+p 1n+q:
30      Shape.FNext{fin_from(p, q, fits)}