You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
chore(idris2): add SPDX headers to idris2/src/*.idr (#134) (#88)
## Summary
Adds the estate-standard 3-line SPDX header (PMPL-1.0-or-later + your
Open.ac.uk copyright) to all 14 Idris2 source files under
\`idris2/src/\`, which were the last \`.idr\` files in the repo without
one.
## Why
\`src/formal/Ephapax/Formal/*.idr\` etc. already use this exact header;
\`idris2/src/*.idr\` were the sole gap. Standards #134 listed this as an
outstanding SPDX-coverage item.
## What
- 14 files touched, 42 insertions, 0 deletions, 0 modifications to
existing lines.
- Header is byte-identical to the existing template (RegionLinear.idr,
Qualifier.idr).
- Trailing newlines preserved.
- Idris2 ignores \`--\` comments before \`module …\`, so the build is
unchanged.
## Test plan
- [x] All 14 files now match the canonical SPDX template
- [x] No existing line modified, no trailing newlines stripped
- [x] Baseline rot in \`ephapax-parse-tests.ipkg\` (\`testLexPositions\`
/ \`parseWithBuf\` undefined) verified pre-existing on \`origin/main\`
and explicitly out of scope
- [ ] Repo CI (license-check + dogfood-gate) goes green
Refs hyperpolymath/standards#124#134
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
0 commit comments