From 1a59b19a615483ade6284e554c53f17afabb7287 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Sun, 5 Apr 2026 16:18:40 +0200
Subject: some cleanup

---
 tools/Scanner/Protocol.lean | 58 ++++++++++++++++++++++-----------------------
 1 file changed, 29 insertions(+), 29 deletions(-)

(limited to 'tools/Scanner/Protocol.lean')

diff --git a/tools/Scanner/Protocol.lean b/tools/Scanner/Protocol.lean
index 6f74126..183ef6a 100644
--- a/tools/Scanner/Protocol.lean
+++ b/tools/Scanner/Protocol.lean
@@ -60,15 +60,15 @@ structure EnumDesc where
   deriving Repr, BEq, Inhabited
 
 inductive ArgumentType where
-| int
-| uInt
-| fixed
-| string
-| array
-| fd
-| newID
-| object
-deriving Repr, BEq, Inhabited
+  | int
+  | uint
+  | fixed
+  | string
+  | array
+  | fd
+  | newID
+  | object
+  deriving Repr, BEq, Inhabited
 
 structure ArgumentDesc where
   name : String
@@ -80,9 +80,9 @@ structure ArgumentDesc where
   deriving Repr, BEq, Inhabited
 
 inductive MessageType where
-| normal
-| destructor
-deriving Repr, BEq, Inhabited
+  | normal
+  | destructor
+  deriving Repr, BEq, Inhabited
 
 structure MessageDesc where
   name : String
@@ -115,12 +115,12 @@ end Raw
 namespace Client
 
 structure InterfaceRef where
-  moduleName : Identifier
-  typeName : Identifier
+  protocol : Identifier
+  interface : Identifier
   deriving Repr, BEq, Ord, Inhabited
 
 structure EnumRef extends InterfaceRef where
-  enumName : Identifier
+  enum : Identifier
   deriving Repr, BEq, Ord, Inhabited
 
 structure EnumEntryDesc where
@@ -140,22 +140,22 @@ structure EnumDesc where
   deriving Repr, BEq, Inhabited
 
 inductive Nullability where
-| nullable
-| notNull
-deriving Repr, BEq, Inhabited
+  | nullable
+  | notNull
+  deriving Repr, BEq, Inhabited
 
 def Nullability.ofAllowNull (allowNull : Bool) : Nullability :=
   if allowNull then .nullable else .notNull
 
 inductive ArgumentType where
-| int (enum : Option EnumRef)
-| uInt (enum : Option EnumRef)
-| fixed
-| string (nullability : Nullability)
-| array
-| fd
-| object (nullability : Nullability) (interface : Option InterfaceRef)
-deriving Repr, BEq, Inhabited
+  | int (enum : Option EnumRef)
+  | uint (enum : Option EnumRef)
+  | fixed
+  | string (nullability : Nullability)
+  | array
+  | fd
+  | object (nullability : Nullability) (interface : Option InterfaceRef)
+  deriving Repr, BEq, Inhabited
 
 structure ArgumentDesc where
   name : Identifier
@@ -175,9 +175,9 @@ structure MessageDesc where
   deriving Repr, BEq, Inhabited
 
 inductive ReturnType where
-| unit
-| object (type : Option InterfaceRef)
-deriving Repr, BEq, Inhabited
+  | unit
+  | object (type : Option InterfaceRef)
+  deriving Repr, BEq, Inhabited
 
 structure RequestDesc extends MessageDesc where
   returnType : ReturnType
-- 
cgit v1.3.1