From ad4d34bba7671fdf75850a312c7eeeaeb990a9d3 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sat, 4 Apr 2026 12:17:35 +0200 Subject: transitive closure of interface dependencies --- tools/Scanner/Parser.lean | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'tools/Scanner/Parser.lean') 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 -- cgit v1.3.1