diff options
| author | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-25 19:40:52 +0200 |
|---|---|---|
| committer | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-25 19:40:52 +0200 |
| commit | fc88c6de225592d8700fe1eb40d870ec8863b57d (patch) | |
| tree | 32e7f842c6ca12b2b5ad1382d15c7acef72665de /lib/kernel/celebration.ml | |
| parent | 4f3af5d6fdc3f5aafe955f88ee9a7788e420b62e (diff) | |
| download | colitur-fc88c6de225592d8700fe1eb40d870ec8863b57d.tar.gz colitur-fc88c6de225592d8700fe1eb40d870ec8863b57d.zip | |
test(of): prove the Tabula is total over 1583-9999
A hand-transcribed 13-entry table is only trustworthy if nothing the engine
constructs falls through it. Sampled property plus an exhaustive sweep behind
COLITUR_EXHAUSTIVE_SWEEP, matching the claim Precedence_ef.band already
carries for RG 91's 28 entries.
Mutation-proved rather than assumed: deleting the entry-13 branch reddens it
on a named date.
Diffstat (limited to 'lib/kernel/celebration.ml')
0 files changed, 0 insertions, 0 deletions