def bq.get_nth

bend-osdev-algo@0.1.0.0 · proof_bsearch.bend:424

import Base
import bend-osdev-array@0.1.0.0/array.bend as A

424def bq.get_nth(xs: List<&2, U32>, m: Nat, h: {Nat.is_lt(m, List.length(&2, U32, xs)) == True{} : Bool}) -> {List.get(&2, U32, xs, m) == Some{A.Arrays.nth(U32, xs, m, 0)} : Maybe<&2, U32>}:
425  match xs m:
426    case Nil{} 0n:
427      Empty.absurd({None{} == Some{0} : Maybe<&2, U32>}, bq.ft(h))
428    case Nil{} 1n+mp:
429      Empty.absurd({None{} == Some{0} : Maybe<&2, U32>}, bq.ft(h))
430    case Con{x, t} 0n:
431      {==}
432    case Con{x, t} 1n+mp:
433      bq.get_nth(t, mp, h)