diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2026-04-04 12:17:35 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2026-04-04 12:17:35 +0200 |
| commit | ad4d34bba7671fdf75850a312c7eeeaeb990a9d3 (patch) | |
| tree | e0ff31e0f1399ecc885b7aef506d2c3e395386d5 /tools/Scanner/Parser.lean | |
| parent | 9d537c6a480bbb8835aaae5c8a5918004442c3c6 (diff) | |
transitive closure of interface dependencies
Diffstat (limited to 'tools/Scanner/Parser.lean')
| -rw-r--r-- | tools/Scanner/Parser.lean | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/tools/Scanner/Parser.lean b/tools/Scanner/Parser.lean index 630b3fc..f89c239 100644 --- a/tools/Scanner/Parser.lean +++ b/tools/Scanner/Parser.lean @@ -2,6 +2,12 @@ import Scanner.Protocol import Lean.Data.Xml.Basic import Lean.Data.Xml.Parser +/-! +# Parsing of Protocol Description + +This converts a protocol description XML into a `Raw.ProtocolDesc`. +-/ + private def String.toNat (s : String) : Except String Nat := match Lean.Syntax.decodeNatLitVal? s with | .some n => .ok n |