0xab5b72f8 checks

0xab5b72f8eac09d083aa0b359ebe0a970

Definitional laws for Vec2.

Anonymous package: import it by hash.

Published: 2026-09-18
Size: 4,217 bytes, 4 files
License: MIT-0 (no LICENSE file; the hub's default)
Declarations: 13 laws (13 proved), 12 defs, 1 types

Import

import 0xab5b72f8eac09d083aa0b359ebe0a970/LAWS.bend as LAWS
import 0xab5b72f8eac09d083aa0b359ebe0a970/PROOF.bend as PROOF
import 0xab5b72f8eac09d083aa0b359ebe0a970/lib.bend as Lib
import 0xab5b72f8eac09d083aa0b359ebe0a970/seal.bend as Seal

Modules

LAWS.bend 13 declarations, 13 laws — Definitional laws for Vec2.
PROOF.bend 0 declarations — Proof witnesses for LAWS.bend. All goals are discharged by normalization.
lib.bend 14 declarations — Vec2 — foundational two-dimensional vectors over Base F32.
seal.bend 0 declarations — Local package seal. Importing the seal checks that laws and proof travel

Dependencies

No imports from other hub packages.

Dependents

No package in this build imports it.

Status on bend 2.0.36

File	Status	Checker says	Time
LAWS.bend	open laws/TODOs	13 TODOs found. Checked alone, a law without a def is a TODO; all of them are proved in files that check, so the package counts this file as checks. output SOME PROOFS FAIL Error: 13 TODOs found. The code is incomplete, and not a valid proof yet.	0.6 s
PROOF.bend	checks	ALL PROOFS CHECK	0.8 s
lib.bend	checks	ALL PROOFS CHECK	0.8 s
seal.bend	checks	ALL PROOFS CHECK	0.7 s