bend-mathlib@0.7.0.0 checks

0x63d5fd78a2a52f082c7824372390170c

bend-mathlib/algebra.bend: abstract associativity/commutativity theorems and their Nat/Bool/List instances.

bend-mathlib@0.7.0.0 by MuhDur

Published

2026-09-29

Size

358,814 bytes, 12 files

License

Apache-2.0 (LICENSE)

Declarations

702 laws (702 proved), 205 defs, 0 types

Import

import bend-mathlib@0.7.0.0/algebra.bend as Algebra
import 0x63d5fd78a2a52f082c7824372390170c/algebra.bend as Algebra
import bend-mathlib@0.7.0.0/all.bend as All
import 0x63d5fd78a2a52f082c7824372390170c/all.bend as All
import bend-mathlib@0.7.0.0/bool.bend as MBool
import 0x63d5fd78a2a52f082c7824372390170c/bool.bend as MBool
import bend-mathlib@0.7.0.0/equal.bend as MEqual
import 0x63d5fd78a2a52f082c7824372390170c/equal.bend as MEqual
import bend-mathlib@0.7.0.0/list.bend as MList
import 0x63d5fd78a2a52f082c7824372390170c/list.bend as MList
import bend-mathlib@0.7.0.0/maybe.bend as MMaybe
import 0x63d5fd78a2a52f082c7824372390170c/maybe.bend as MMaybe
import bend-mathlib@0.7.0.0/nat.bend as MNat
import 0x63d5fd78a2a52f082c7824372390170c/nat.bend as MNat
import bend-mathlib@0.7.0.0/order.bend as Order
import 0x63d5fd78a2a52f082c7824372390170c/order.bend as Order
import bend-mathlib@0.7.0.0/perm.bend as Perm
import 0x63d5fd78a2a52f082c7824372390170c/perm.bend as Perm
import bend-mathlib@0.7.0.0/sort.bend as Sort
import 0x63d5fd78a2a52f082c7824372390170c/sort.bend as Sort
import bend-mathlib@0.7.0.0/string.bend as MString
import 0x63d5fd78a2a52f082c7824372390170c/string.bend as MString

Modules

• algebra.bend 45 declarations, 34 laws — bend-mathlib/algebra.bend: abstract associativity/commutativity theorems and their Nat/Bool/List instances.
• all.bend 0 declarations — bend-mathlib: machine-checked lemmas for Bend 2 (Nat, Bool, List, String, Maybe, equality); import one module, e.g. bend-mathlib@0.7.0.0/nat.bend.
• bool.bend 71 declarations, 69 laws — bend-mathlib/bool.bend: Bool algebra (not, and, or, xor).
• equal.bend 4 declarations, 4 laws — bend-mathlib/equal.bend: equality lemmas (congruence, substitution, chains).
• list.bend 230 declarations, 194 laws — bend-mathlib/list.bend: List lemmas (append, reverse, length, take, drop, map, fold, filter).
• maybe.bend 30 declarations, 30 laws — bend-mathlib/maybe.bend: Maybe monad and map laws over &2.
• nat.bend 361 declarations, 314 laws — bend-mathlib/nat.bend: Nat arithmetic (add, mul, sub, min, max, pow) and order (le, lt, ge, gt).
• order.bend 7 declarations, 6 laws — bend-mathlib/order.bend: abstract preorder/total-order facts over a Bool comparator ~le.
• perm.bend 52 declarations — bend-mathlib/perm.bend: step-list permutations over bendlib-kernel-list, plus sort value defs and proofs.
• sort.bend 37 declarations — bend-mathlib/sort.bend: insertion and merge sort proved sorted over perm.bend's value defs (generic ~le).
• string.bend 70 declarations, 51 laws — bend-mathlib/string.bend: String append, reverse and length, and comparison.

Other files

• LICENSE 11,381 bytes

Dependencies

• bendlib-kernel-list@1.0.0.0 via perm.bend: import 0xb5c8145e53a6a127d611f45f602666ec/list.bend as K

Dependents

• mylsm-lsm-store@0.5.0.0 via src/Keys.bend: import bend-mathlib@0.7.0.0/string.bend as MString
• mylsm-lsm-store@0.4.0.0 via src/Keys.bend: import bend-mathlib@0.7.0.0/string.bend as MString

Status on bend 2.0.36