def Fin.bound

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

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

import Base

45def Fin.bound(+n: Nat, +index: Fin(n)) -> LT(Fin.value(n, index), n):
46  match n:
47    case 0n:
48      match index:
49    case 1n+k:
50      match index:
51        case FZero{}:
52          Unit{}
53        case FNext{+previous}:
54          Fin.bound(k, previous)

Uses (6)

Used by (4)