ABI: make Idris2 proofs genuinely compile + add machine-checked theorems#31

Merged

hyperpolymath merged 3 commits into

mainfrom

claude/iseriser-proofs-review-rtdcwb

Jun 26, 2026

Commits on Jun 26, 2026

Add SPDX header to LICENSE and set Cargo.toml license field

Jonathan D.A. Jewell
and
claude
committed
Normalize licensing to MPL-2.0 (code) + CC-BY-SA-4.0 (docs)

Jonathan D.A. Jewell
and
claude
committed
Fix Idris2 ABI proofs so they genuinely compile and verify
claude
committed