def bq.get_take

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

import Base

411def bq.get_take(xs: List<&2, U32>, k: Nat, m: Nat, h: {Nat.is_lt(m, k) == True{} : Bool}) -> {List.get(&2, U32, List.take(&2, U32, xs, k), m) == List.get(&2, U32, xs, m) : Maybe<&2, U32>}:
412  match xs k m:
413    case Nil{} _ _:
414      {==}
415    case Con{x, t} 0n 0n:
416      Empty.absurd({List.get(&2, U32, List.take(&2, U32, Con{x, t}, 0n), 0n) == List.get(&2, U32, Con{x, t}, 0n) : Maybe<&2, U32>}, bq.ft(h))
417    case Con{x, t} 0n 1n+mp:
418      Empty.absurd({List.get(&2, U32, List.take(&2, U32, Con{x, t}, 0n), 1n+mp) == List.get(&2, U32, Con{x, t}, 1n+mp) : Maybe<&2, U32>}, bq.ft(h))
419    case Con{x, t} 1n+kp 0n:
420      {==}
421    case Con{x, t} 1n+kp 1n+mp:
422      bq.get_take(t, kp, mp, h)