def drop_nil

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/tree.bend:157

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend as LS

157# The drop is empty exactly when the list fits.
158def drop_nil(+xs: List<&2,T.Out>, +k: Nat) -> {S.is_nil(SC.drop(T.Out,xs,k)) == Nat.is_le(SC.length(T.Out,xs),k) : Bool}:
159  %Equal.sym(Bool,S.is_nil(SC.drop(T.Out,xs,k)),LS.is_empty(T.Out,SC.drop(T.Out,xs,k)),nil_is_empty(SC.drop(T.Out,xs,k))) : {_ == Nat.is_le(SC.length(T.Out,xs),k) : Bool}
160  LS.empty_drop(T.Out,xs,k)