Wide.zero: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend as Wide Lines 4-6 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend&start_line=4&end_line=6 import Base # All bits are represented explicitly: no Nat holds a full-width integer. def zero() -> Word(64n): Word.zero(64n) Uses (2): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero