def pow_ne

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

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/proofs/lib/logic.bend as L
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

169def pow_ne(+xs: List<&2,T.Out>, +p: Nat, +hl: {SC.length(T.Out,xs) == SC.pow2(p) : Nat}) -> {S.is_nil(xs) == False{} : Bool}:
170  match xs:
171    case Nil{}: Empty.absurd({S.is_nil(Nil{}) == False{} : Bool},L.false_true(zero_pow(p,hl)))
172    case Con{+x,+r}: {==}