0xd5e93625 checks

0xd5e9362591c1667c9894b781190e1ac9

no description

Anonymous package: import it by hash.

Published

2026-09-17

Size

251,708 bytes, 12 files

License

MIT-0 (no LICENSE file; the hub's default)

Declarations

33 laws (33 proved), 440 defs, 10 types

Import

import 0xd5e9362591c1667c9894b781190e1ac9/euclid.bend as Euclid
import 0xd5e9362591c1667c9894b781190e1ac9/fermat4.bend as Fermat4
import 0xd5e9362591c1667c9894b781190e1ac9/gcd.bend as Gcd
import 0xd5e9362591c1667c9894b781190e1ac9/int.bend as Int
import 0xd5e9362591c1667c9894b781190e1ac9/int_filled.bend as Int_filled
import 0xd5e9362591c1667c9894b781190e1ac9/math.bend as Math
import 0xd5e9362591c1667c9894b781190e1ac9/mathlib.bend as Mathlib
import 0xd5e9362591c1667c9894b781190e1ac9/nat.bend as MNat
import 0xd5e9362591c1667c9894b781190e1ac9/primes.bend as Primes
import 0xd5e9362591c1667c9894b781190e1ac9/pythag.bend as Pythag
import 0xd5e9362591c1667c9894b781190e1ac9/reals.bend as Reals
import 0xd5e9362591c1667c9894b781190e1ac9/sqrt2.bend as Sqrt2

Modules

• euclid.bend 40 declarations
• fermat4.bend 41 declarations — demos/math/fermat4.bend -- Fermat's Last Theorem for exponent 4.
• gcd.bend 103 declarations — lib/gcd.bend -- divisibility, Bezout coprimality, Euclid's algorithm, and
• int.bend 39 declarations, 33 laws — int.bend -- the integers, as a bounty: a canonical
• int_filled.bend 49 declarations
• math.bend 0 declarations — # The bend.how number library, as one package.
• mathlib.bend 34 declarations — Arithmetic for the proofs: addition, multiplication, equality, squares.
• nat.bend 68 declarations — lib/nat.bend -- the arithmetic of Base's Nat, as theorems.
• primes.bend 21 declarations — lib/primes.bend -- the structural number theory behind Euclid's theorem.
• pythag.bend 37 declarations — lib/pythag.bend -- primitive Pythagorean triples, on top of lib/gcd.bend.
• reals.bend 50 declarations — 0.999... = 1 -- a machine-checked proof, in one file.
• sqrt2.bend 14 declarations — lib/sqrt2.bend -- the square root of 2 is irrational, from lib/nat.bend.

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: 33 TODOs found.
The code is incomplete, and not a valid proof yet.