Skip to content

Commit e50b18b

Browse files
hyperpolymathclaude
andcommitted
proof(xml-7-44): rename prefix field → nsPrefix (0.8.0 keyword clash)
`Xml744.Document.Namespace.prefix` collided with Idris2 0.8.0's `prefix` reserved word for operator-section syntax, parsing as "Expected end of input" at the field declaration. Renamed the field to `nsPrefix` and updated the one consumer (`renderNs`). Pure rename, no semantic change. With this in place, `Xml744.Document` compiles (5/6) and `Xml744.Core` compiles (6/6) — the whole toolkit is green for the first time since the rescue extraction in commit `0c78bfce`. All 12 exports across the two files check `is total` and no `assert_total` / `assert_smaller` / `believe_me` / `%unsafe` / `PROOF_TODO` / `idris_crash` / `partial ` markers remain in any of the six toolkit modules. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 6323136 commit e50b18b

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)