Skip to content

Commit 087421b

Browse files
proof(xml-7-44): rename Namespace.prefix → nsPrefix (Idris2 0.8.0 keyword) (#82)
## Summary One-line rename to clear the final baseline-rot blocker in the idris2-xml toolkit. `Xml744.Document.Namespace.prefix` collides with Idris2 0.8.0's `prefix` reserved word for operator-section syntax — the field declaration parses as "Expected end of input". Renamed the field to `nsPrefix` and updated the one consumer (`renderNs`). Pure rename, no semantic change. ## Result: toolkit fully green With #79 + #80 + #81 + this branch, every module builds: ``` 1/6: Building Xml744.Escape 2/6: Building Xml744.Text 3/6: Building Xml744.Attribute 4/6: Building Xml744.Element 5/6: Building Xml744.Document 6/6: Building Xml744.Core ``` First clean build since the rescue extraction in commit `0c78bfce`. 12 exports across `Document` + `Core` check `is total`. Across the full toolkit: ``` $ grep -nE 'assert_total|assert_smaller|believe_me|%unsafe|PROOF_TODO|idris_crash|partial ' src/Xml744/*.idr | grep -v 'without `assert' (no matches — only doc-comment mentions describing what is NOT used) ``` Total damage to land all six green: 4 PRs touching 4 files; 9 proof debts retired; 40 exported names verified `is total`; zero proof escapes remain. ## Stack Stacks on top of #81#80#79. Base is `main` per the orphan-trap guidance, so the diff is cumulative until the earlier PRs land, then this rebases to a 4-line single-file change. ## Test plan - [ ] CI green - [ ] `idris2 --build idris2-ecosystem/xml-toolkit/xml-7-44.ipkg` reports 6/6 modules built (verified locally) 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 094750c commit 087421b

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

idris2-ecosystem/xml-toolkit/src/Xml744/Document.idr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ renderDecl d =
3434
public export
3535
record Namespace where
3636
constructor MkNs
37-
prefix : String
37+
nsPrefix : String
3838
uri : String
3939

4040
||| Common OOXML namespaces
@@ -53,7 +53,7 @@ nsMarkupCompat = MkNs "mc" "http://schemas.openxmlformats.org/markup-compatibili
5353
||| Render namespace as attribute
5454
export
5555
renderNs : Namespace -> String
56-
renderNs ns = "xmlns:" ++ ns.prefix ++ "=\"" ++ ns.uri ++ "\""
56+
renderNs ns = "xmlns:" ++ ns.nsPrefix ++ "=\"" ++ ns.uri ++ "\""
5757

5858
||| Full XML document
5959
public export

0 commit comments

Comments
 (0)