0xb13667d5 checks

0xb13667d52aa56e002b4d09883d7fce3e

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

Anonymous package: import it by hash.

Published

2026-09-26

Size

80,273 bytes, 7 files

License

MIT (LICENSE)

Declarations

44 laws (44 proved), 81 defs, 1 types

Import

import 0xb13667d52aa56e002b4d09883d7fce3e/LAWS.bend as LAWS
import 0xb13667d52aa56e002b4d09883d7fce3e/PROOF.bend as PROOF
import 0xb13667d52aa56e002b4d09883d7fce3e/ac.bend as Ac
import 0xb13667d52aa56e002b4d09883d7fce3e/mul.bend as Mul
import 0xb13667d52aa56e002b4d09883d7fce3e/nat.bend as MNat
import 0xb13667d52aa56e002b4d09883d7fce3e/word.bend as MWord

Modules

• LAWS.bend 44 declarations, 44 laws — wordlib: laws about Base's fixed-width words. Word(n) is n Bools,
• PROOF.bend 36 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,
• mul.bend 8 declarations — mul.bend: laws of Base's Nat.mul. Kept apart from nat.bend because the
• nat.bend 19 declarations — nat.bend: laws of Base's Nat.add, Nat.mul and Nat.double, as typed defs.
• word.bend 8 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: 44 TODOs found.
The code is incomplete, and not a valid proof yet.