ProofBsearch.bq.get_nth: def of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as ProofBsearch
Lines 424-433 of bend-osdev-algo@0.1.0.0/proof_bsearch.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&start_line=424&end_line=433

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

def 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>}:
  match xs m:
    case Nil{} 0n:
      Empty.absurd({None{} == Some{0} : Maybe<&2, U32>}, bq.ft(h))
    case Nil{} 1n+mp:
      Empty.absurd({None{} == Some{0} : Maybe<&2, U32>}, bq.ft(h))
    case Con{x, t} 0n:
      {==}
    case Con{x, t} 1n+mp:
      bq.get_nth(t, mp, h)

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.ft
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.nth