0xe6b82fa6 fails
0xe6b82fa6c4c459c7023adf4b12a3ac46
LAWS.bend -- the laws of tinygrad, stated for the Bend port.
Anonymous package: import it by hash.
- Published
- 2026-09-19
- Size
- 44,718 bytes, 6 files
- License
- MIT-0 (no LICENSE file; the hub's default)
- Declarations
- 5 laws (5 proved), 33 defs, 0 types
Import
import 0xe6b82fa6c4c459c7023adf4b12a3ac46/LAWS.bend as LAWS import 0xe6b82fa6c4c459c7023adf4b12a3ac46/PROOF.bend as PROOF import 0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad.bend as Tinygrad import 0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/nat.bend as MNat import 0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.bend as Shape import 0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/tensor.bend as Tensor
Modules
- LAWS.bend 5 declarations, 5 laws — LAWS.bend -- the laws of tinygrad, stated for the Bend port.
- PROOF.bend 5 declarations — PROOF.bend -- proofs of the laws in LAWS.bend. The gate:
- tinygrad.bend not loaded — tinygrad.bend -- root of the tinygrad Bend port. Importing this file
- tinygrad/nat.bend 7 declarations — tinygrad/nat.bend -- arithmetic lemmas over Nat used by PROOF.bend.
- tinygrad/shape.bend 21 declarations — tinygrad/shape.bend -- pure shape arithmetic for tinygrad-bend.
- tinygrad/tensor.bend not loaded — tinygrad/tensor.bend -- the lazy tensor core of tinygrad-bend.
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 | 5 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. outputSOME PROOFS FAIL Error: 5 TODOs found. The code is incomplete, and not a valid proof yet. | 0.9 s |
| PROOF.bend | checks | ALL PROOFS CHECK | 0.8 s |
| tinygrad.bend | fails | - message : a type for this operator (write (a * b : Nat))outputError:
- message : a type for this operator (write (a * b : Nat))
Location:
201 | +c = row_width(rows)
202>| fill_from_list(r*c, flat, 0n, alloc(r*c), matrix_shape(r, c))
| ^
203 |
Note: we broke this after launch, sorry. Until 2.0.16 a bare operator meant Nat.
That was a bug: operators demand annotation. Wrap the expression and it'll work again. | 0.5 s |
| tinygrad/nat.bend | checks | ALL PROOFS CHECK | 0.7 s |
| tinygrad/shape.bend | checks | ALL PROOFS CHECK | 0.8 s |
| tinygrad/tensor.bend | fails | - message : a type for this operator (write (a * b : Nat))outputError:
- message : a type for this operator (write (a * b : Nat))
Location:
201 | +c = row_width(rows)
202>| fill_from_list(r*c, flat, 0n, alloc(r*c), matrix_shape(r, c))
| ^
203 |
Note: we broke this after launch, sorry. Until 2.0.16 a bare operator meant Nat.
That was a bug: operators demand annotation. Wrap the expression and it'll work again. | 0.4 s |