def nth_lt_length

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/list.bend:109

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

109def nth_lt_length(-A: Data, +xs: List<&2, A>, +i: Nat, +x: A, +h: {SC.nth(A, xs, i) == Some{x} : Maybe<&2, A>}) -> {Nat.is_lt(i, SC.length(A, xs)) == True{} : Bool}:
110  match xs i:
111    case Nil{} _:
112      Empty.absurd({Nat.is_lt(i, 0n) == True{} : Bool}, L.none_some(A, x, h))
113    case Con{h1, t} 0n:
114      {==}
115    case Con{h1, t} 1n+p:
116      nth_lt_length(A, t, p, x, h)