law take_nil_ev

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/value.bend:270

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend as Value
import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend as Li

270law take_nil_ev:
271  for +n: Nat
272  {ev(Li.take(n, [])) == 0n : Nat}

Uses (4)

Used by (1)