bend-mathlib@0.4.0.0 fails

0xfa8bcf3897afe3da6c28dd6f9de6cbea

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

bend-mathlib@0.4.0.0 by MuhDur

Other versions (9)

Published: 2026-09-28
Size: 214,168 bytes, 12 files
License: Apache-2.0 (LICENSE)
Declarations: 389 laws (76 proved), 170 defs, 0 types

Import

import bend-mathlib@0.4.0.0/algebra.bend as Algebra
import 0xfa8bcf3897afe3da6c28dd6f9de6cbea/algebra.bend as Algebra
import bend-mathlib@0.4.0.0/all.bend as All
import 0xfa8bcf3897afe3da6c28dd6f9de6cbea/all.bend as All
import bend-mathlib@0.4.0.0/bool.bend as MBool
import 0xfa8bcf3897afe3da6c28dd6f9de6cbea/bool.bend as MBool
import bend-mathlib@0.4.0.0/equal.bend as MEqual
import 0xfa8bcf3897afe3da6c28dd6f9de6cbea/equal.bend as MEqual
import bend-mathlib@0.4.0.0/list.bend as MList
import 0xfa8bcf3897afe3da6c28dd6f9de6cbea/list.bend as MList
import bend-mathlib@0.4.0.0/maybe.bend as MMaybe
import 0xfa8bcf3897afe3da6c28dd6f9de6cbea/maybe.bend as MMaybe
import bend-mathlib@0.4.0.0/nat.bend as MNat
import 0xfa8bcf3897afe3da6c28dd6f9de6cbea/nat.bend as MNat
import bend-mathlib@0.4.0.0/order.bend as Order
import 0xfa8bcf3897afe3da6c28dd6f9de6cbea/order.bend as Order
import bend-mathlib@0.4.0.0/perm.bend as Perm
import 0xfa8bcf3897afe3da6c28dd6f9de6cbea/perm.bend as Perm
import bend-mathlib@0.4.0.0/sort.bend as Sort
import 0xfa8bcf3897afe3da6c28dd6f9de6cbea/sort.bend as Sort
import bend-mathlib@0.4.0.0/string.bend as MString
import 0xfa8bcf3897afe3da6c28dd6f9de6cbea/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, equality); import one module, e.g. bend-mathlib@0.4.0.0/nat.bend.
bool.bend 64 declarations, 62 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 105 declarations, 89 laws — bend-mathlib/list.bend: List lemmas (append, reverse, length, take, drop, map, fold, filter).
maybe.bend 10 declarations, 10 laws — bend-mathlib/maybe.bend: Maybe monad and map laws over &2.
nat.bend 193 declarations, 159 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 42 declarations, 25 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

No package in this build imports it.

Status on bend 2.0.36

File	Status	Checker says	Time
algebra.bend	fails	- expected : a defined name output Error: - expected : a defined name - observed : Nat.div.fin Context: - n : Nat - m : Nat - bp : Nat - d : Nat - r : Nat - h : {bp == Nat.add(r, m) : Nat} Location: internal_div_go_eq 759 \| 760>\| def internal_div_go_eq(n: Nat, m: Nat, +bp: Nat, +d: Nat, +r: Nat, +h: {bp == Nat.add(r, m) : Nat}) -> {Nat.add(Nat.mul(Nat.div.fin(Nat.divmod.go(n, m, d, r)), 1n+bp), Nat.mod.fin(Nat.divmod.go(n, m, d, r))) == Nat.add(n, Nat.add(Nat.mul(d, 1n+bp), r)) : Nat}: \| ^^^^^^^^^^^ 761 \| match n m:	0.8 s
all.bend	fails	- expected : a defined name output Error: - expected : a defined name - observed : Nat.div.fin Context: - n : Nat - m : Nat - bp : Nat - d : Nat - r : Nat - h : {bp == Nat.add(r, m) : Nat} Location: internal_div_go_eq 759 \| 760>\| def internal_div_go_eq(n: Nat, m: Nat, +bp: Nat, +d: Nat, +r: Nat, +h: {bp == Nat.add(r, m) : Nat}) -> {Nat.add(Nat.mul(Nat.div.fin(Nat.divmod.go(n, m, d, r)), 1n+bp), Nat.mod.fin(Nat.divmod.go(n, m, d, r))) == Nat.add(n, Nat.add(Nat.mul(d, 1n+bp), r)) : Nat}: \| ^^^^^^^^^^^ 761 \| match n m:	0.9 s
bool.bend	checks	ALL PROOFS CHECK	1.0 s
equal.bend	checks	ALL PROOFS CHECK	0.8 s
list.bend	fails	- expected : a defined name output Error: - expected : a defined name - observed : Nat.div.fin Context: - n : Nat - m : Nat - bp : Nat - d : Nat - r : Nat - h : {bp == Nat.add(r, m) : Nat} Location: internal_div_go_eq 759 \| 760>\| def internal_div_go_eq(n: Nat, m: Nat, +bp: Nat, +d: Nat, +r: Nat, +h: {bp == Nat.add(r, m) : Nat}) -> {Nat.add(Nat.mul(Nat.div.fin(Nat.divmod.go(n, m, d, r)), 1n+bp), Nat.mod.fin(Nat.divmod.go(n, m, d, r))) == Nat.add(n, Nat.add(Nat.mul(d, 1n+bp), r)) : Nat}: \| ^^^^^^^^^^^ 761 \| match n m:	1.0 s
maybe.bend	checks	ALL PROOFS CHECK	0.7 s
nat.bend	fails	- expected : a defined name output Error: - expected : a defined name - observed : Nat.div.fin Context: - n : Nat - m : Nat - bp : Nat - d : Nat - r : Nat - h : {bp == Nat.add(r, m) : Nat} Location: internal_div_go_eq 759 \| 760>\| def internal_div_go_eq(n: Nat, m: Nat, +bp: Nat, +d: Nat, +r: Nat, +h: {bp == Nat.add(r, m) : Nat}) -> {Nat.add(Nat.mul(Nat.div.fin(Nat.divmod.go(n, m, d, r)), 1n+bp), Nat.mod.fin(Nat.divmod.go(n, m, d, r))) == Nat.add(n, Nat.add(Nat.mul(d, 1n+bp), r)) : Nat}: \| ^^^^^^^^^^^ 761 \| match n m:	0.9 s
order.bend	fails	- expected : a defined name output Error: - expected : a defined name - observed : Nat.div.fin Context: - n : Nat - m : Nat - bp : Nat - d : Nat - r : Nat - h : {bp == Nat.add(r, m) : Nat} Location: internal_div_go_eq 759 \| 760>\| def internal_div_go_eq(n: Nat, m: Nat, +bp: Nat, +d: Nat, +r: Nat, +h: {bp == Nat.add(r, m) : Nat}) -> {Nat.add(Nat.mul(Nat.div.fin(Nat.divmod.go(n, m, d, r)), 1n+bp), Nat.mod.fin(Nat.divmod.go(n, m, d, r))) == Nat.add(n, Nat.add(Nat.mul(d, 1n+bp), r)) : Nat}: \| ^^^^^^^^^^^ 761 \| match n m:	1.0 s
perm.bend	checks	ALL PROOFS CHECK	0.9 s
sort.bend	fails	- expected : a defined name output Error: - expected : a defined name - observed : Nat.div.fin Context: - n : Nat - m : Nat - bp : Nat - d : Nat - r : Nat - h : {bp == Nat.add(r, m) : Nat} Location: internal_div_go_eq 759 \| 760>\| def internal_div_go_eq(n: Nat, m: Nat, +bp: Nat, +d: Nat, +r: Nat, +h: {bp == Nat.add(r, m) : Nat}) -> {Nat.add(Nat.mul(Nat.div.fin(Nat.divmod.go(n, m, d, r)), 1n+bp), Nat.mod.fin(Nat.divmod.go(n, m, d, r))) == Nat.add(n, Nat.add(Nat.mul(d, 1n+bp), r)) : Nat}: \| ^^^^^^^^^^^ 761 \| match n m:	1.0 s
string.bend	fails	- expected : a defined name output Error: - expected : a defined name - observed : String.eq.fin Context: - s : String - _ : Sigma<&1, &1, Sigma<&1, &1, String, _ => String>, _ => Cmp> - : {((s, s), EQ{}) == _ : Sigma<&1, &1, Sigma<&1, &1, String, _ => String>, _ => Cmp>} Location: eq_refl 190 \| def eq_refl(s): 191>\| %internal_cmp_refl(s) : {String.eq.fin(_) == True{} : Bool} \| ^^^^^^^^^^^^^ 192 \| {==}	0.9 s