def nth_some

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/words32.bend:59

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

59def nth_some(+tb: List<&2, U32>, +i: Nat, +h: {Nat.is_lt(i, SC.length(U32, tb)) == True{} : Bool}) -> {SC.nth(U32, tb, i) == Some{nth0(tb, i)} : Maybe<&2, U32>}:
60  match tb i:
61    case Nil{} _:
62      Empty.absurd({SC.nth(U32, Nil{}, i) == Some{nth0(Nil{}, i)} : Maybe<&2, U32>}, N.lt_zero_absurd(i, h))
63    case Con{x, t} 0n:
64      {==}
65    case Con{x, t} 1n+p:
66      nth_some(t, p, h)