← bend.how

The bend.how library

Bend ships its own standard library. These files are not part of it, and are not going to be merged into it. They live here so that anything on this site, and anything your agent builds after reading it, has somewhere to get them.

Everything here is plain Bend. Put the files next to your program and import them.

math/ — numbers and the proofs about them

Self-contained: every import inside these files is relative, so copying the folder is enough.

file	what is in it
nat.bend	naturals: addition, multiplication, order, and a subtraction that stays symbolic
mathlib.bend	the scaffolding the proofs lean on: the ladder behind add_comm, doubling, parity
int.bend	integers
int_filled.bend	the same, with the proofs filled in
reals.bend	reals as Cauchy sequences — enough to prove 0.999… = 1
primes.bend	primality, factors, and that there is no largest prime
gcd.bend	greatest common divisor
euclid.bend	Euclid's algorithm, with the descent argument
sqrt2.bend	the irrationality of √2, by descent
pythag.bend	Pythagorean triples
fermat4.bend	Fermat's last theorem for n = 4
math.bend	the hub entry file: imports the eleven files above in one place, so bend math.bend --publish ships them under one hash. Not loaded by the editor
LAWS.bend	the claim board: what is proved, what is refuted, what is still open
PROOF.bend	the proofs of those laws, one def per law; bend PROOF.bend is the gate

The editor at /math/ loads all of these except math.bend — it runs bend PROOF.bend, which never imports the umbrella — and runs the real checker over them in your browser.

fixed/ — arithmetic for deep zooms

fixed64.bend and fx4.bend import only Base.

file	what is in it
fixed64.bend	a 64-bit fixed-point number: the workhorse once 32-bit floats stop resolving the detail
fx4.bend	four-limb fixed point, for when 64 bits stop being enough either
fixed.bend	the hub entry file: imports both of the above, so bend fixed.bend --publish ships them under one hash

chess/ — a four by four game, under one law

Written and checking. White cannot win on the first turn, and that is proved by playing every first move and every reply, which on this board the checker can simply do.

file	what is in it
chess.bend	squares as numbers 0 to 15, and how a king, a pawn, a queen and a knight step on an empty board
game.bend	the game: occupancy, captures, lines of sight, check, mate, stalemate, and the two opening positions
LAWS.bend	the laws. Five about single positions are proved; seven about every square and every board are open
PROOF.bend	the proofs, one def per law; bend PROOF.bend is the gate
README.md	what is proved, what is open, and the traps already measured

bend PROOF.bend stops at Error: 7 TODOs found., the seven open laws. Open it in the editor — two claims about movement are false on purpose, and uncommenting either sets the search looking for the pair of squares that breaks it.

From the hub

The parts that check clean are also on Bend's hub, one content-hash package each; import a package's file by its path and the first run fetches and verifies it.

# nat, mathlib, int, int_filled, reals, primes, euclid, sqrt2, gcd, pythag, fermat4
import 0xd5e9362591c1667c9894b781190e1ac9/math.bend as Math
# fixed64, fx4
import 0x4e6a6615b0feb5ac27adea952228511e/fixed.bend as Fixed
# chess, game
import 0x6d15da24c6555ddee2181d043774a796/game.bend as Game

The claim boards (LAWS.bend, PROOF.bend) are not on the hub: it refuses a file with an open law, and those files keep the open ones on purpose. Fetch them from here.

Fetching them

The site serves this folder, so an agent can pull what it needs directly:

mkdir -p lib/math && cd lib/math
curl -fsSL --remote-name-all "https://bend.how/lib/math/{nat,mathlib,sqrt2}.bend"

Every red button on the front page hands your agent the right version of that command, together with Bend itself.