def get

stelliferous@0.0.2.0 · math_sequence.bend:46

import Base

46def get(-Element: Data,length: Nat,index: Index(length),vector: Values(Element,length)) -> Element:
47  match length:
48    case 0n:
49      match index:
50    case 1n+rest:
51      match index:
52        case First{}:
53          Elements{head,tail} = vector
54          head
55        case Next{index}:
56          Elements{head,tail} = vector
57          get(Element,rest,index,tail)