def index_value

stelliferous@0.0.2.0 · math_sequence.bend:31

import Base

31def index_value(length: Nat,index: Index(length)) -> Nat:
32  match length:
33    case 0n:
34      match index:
35    case 1n+rest:
36      match index:
37        case First{}: 0n
38        case Next{index}: 1n+index_value(rest,index)