0x340691c4 checks

0x340691c4c9cfde2764a3ed46e48d644a

wordlib: laws about Base's fixed-width words. Word(n) is n Bools,

Anonymous package: import it by hash.

Published

2026-09-26

Size

62,588 bytes, 6 files

License

MIT (LICENSE)

Declarations

39 laws (39 proved), 67 defs, 1 types

Import

import 0x340691c4c9cfde2764a3ed46e48d644a/LAWS.bend as LAWS
import 0x340691c4c9cfde2764a3ed46e48d644a/PROOF.bend as PROOF
import 0x340691c4c9cfde2764a3ed46e48d644a/ac.bend as Ac
import 0x340691c4c9cfde2764a3ed46e48d644a/nat.bend as MNat
import 0x340691c4c9cfde2764a3ed46e48d644a/word.bend as MWord

Modules

• LAWS.bend 39 declarations, 39 laws — wordlib: laws about Base's fixed-width words. Word(n) is n Bools,
• PROOF.bend 31 declarations — wordlib: the proofs of LAWS.bend. Each word law is an induction on the
• ac.bend 15 declarations — ac.bend: sums over Nat decided by reflection. An Expr is a sum of atoms,
• nat.bend 19 declarations — nat.bend: laws of Base's Nat.add, Nat.mul and Nat.double, as typed defs.
• word.bend 7 declarations — word.bend: the vocabulary wordlib's laws are stated in.

Other files

• LICENSE 1,066 bytes

Dependencies

No imports from other hub packages.

Dependents

No package in this build imports it.

Status on bend 2.0.36

SOME PROOFS FAIL
Error: 39 TODOs found.
The code is incomplete, and not a valid proof yet.