style: apply the signature layout

EventB/Embedding.lean

@@ -15,7 +15,11 @@ abbrev EventSet (α : Type) := α → Prop
 structure Signature where
   carrier : String → Type
 
-private def typeOf? (signature : Signature) : Typing.Ty → Option Type
+private
+def typeOf?
+    (signature : Signature)
+    : Typing.Ty →
+      Option Type
   | .given name => some (signature.carrier name)
   | .int => some Int
   | .bool => some Bool
@@ -26,13 +30,25 @@ private def typeOf? (signature : Signature) : Typing.Ty → Option Type
       return left × right
   | .mvar _ => none
 
-def type? (signature : Signature) (type : Typing.Ty) : Option Type :=
+def type?
+    (signature : Signature)
+    (type : Typing.Ty)
+    : Option Type
+    :=
   typeOf? signature type
 
-def symbolType? (signature : Signature) (symbol : Prelude.Symbol) : Option Type :=
+def symbolType?
+    (signature : Signature)
+    (symbol : Prelude.Symbol)
+    : Option Type
+    :=
   symbol.type.bind (type? signature)
 
-def embeddable (signature : Signature) (env : Theory.Env) : List String :=
+def embeddable
+    (signature : Signature)
+    (env : Theory.Env)
+    : List String
+    :=
   env.theories.flatMap fun theory =>
     theory.symbols.filterMap fun symbol =>
       if symbol.type.isSome && (symbolType? signature symbol).isNone then

EventB/Error.lean

@@ -46,16 +46,29 @@ def io (message : String) : Error := { kind := .io, message }
 
 def cli (message : String) : Error := { kind := .cli, message }
 
-def withPath (error : Error) (path : String) : Error :=
+def withPath
+    (error : Error)
+    (path : String)
+    : Error
+    :=
   { error with path := some path }
 
-def withContext (error : Error) (context : String) : Error :=
+def withContext
+    (error : Error)
+    (context : String)
+    : Error
+    :=
   { error with context := context :: error.context }
 
-def render (error : Error) : String :=
+def render
+    (error : Error)
+    : String
+    :=
   String.intercalate ": " (error.path.toList ++ error.context.reverse ++ [error.message])
 
-instance : ToString Error where
+instance
+    : ToString Error
+    where
   toString := render
 
 end Error

EventB/Formula/Lex.lean

@@ -19,14 +19,18 @@ inductive Tok where
   | op  : String → Tok
   deriving BEq, Repr, Inhabited
 
-def Tok.render : Tok → String
+def Tok.render
+    : Tok →
+      String
   | .id s  => s
   | .num n => toString n
   | .op s  => s
 
 /-- Alias to canonical spelling. Longest match wins, so order here does not matter, but
 every canonical operator must also map to itself. -/
-def operators : List (String × String) :=
+def operators
+    : List (String × String)
+    :=
   -- Predicate calculus.
   [("⇔", "⇔"), ("<=>", "⇔"), ("⇒", "⇒"), ("=>", "⇒"),
    ("∧", "∧"), ("&", "∧"), ("∨", "∨"), ("or", "∨"), ("¬", "¬"), ("not", "¬"),
@@ -75,7 +79,9 @@ def operators : List (String × String) :=
 /-- Longest first, so `<<:` is never read as `<` followed by `<:`. Held as a `Char`
 list per alias because the scanner works on `List Char`, and sorted once: re-sorting a
 130-entry table on every token turned the corpus scan into minutes. -/
-def operatorTable : Array (List Char × String) :=
+def operatorTable
+    : Array (List Char × String)
+    :=
   (operators.mergeSort (fun a b => b.1.length < a.1.length)).map
     (fun (alias, canon) => (alias.toList, canon)) |>.toArray
 
@@ -84,16 +90,24 @@ private def isIdentRest (c : Char) : Bool := c.isAlphanum || c == '_' || c == '\
 
 /-- Operator aliases spelled with letters (`or`, `mod`, `NAT`) must not swallow the head
 of an identifier: `order` is one name, not `or` followed by `der`. -/
-private def aliasFits (alias rest : List Char) : Bool :=
+private
+def aliasFits
+    (alias rest : List Char)
+    : Bool
+    :=
   if alias.all isIdentRest then
     match rest.drop alias.length with
     | c :: _ => !isIdentRest c
     | [] => true
   else
     true
 
-private def matchOperator (table : Array (List Char × String)) (cs : List Char) :
-    Option (String × List Char) :=
+private
+def matchOperator
+    (table : Array (List Char × String))
+    (cs : List Char)
+    : Option (String × List Char)
+    :=
   table.findSome? fun (a, canon) =>
     -- `!a.isEmpty` is load-bearing: an empty alias matches everywhere and consumes
     -- nothing, so the scanner would spin forever on the first character.
@@ -113,8 +127,13 @@ private def matchOperator (table : Array (List Char × String)) (cs : List Char)
 -- This is the obligation grip discharges by construction: its graded parsers track in
 -- the type whether a parser can consume nothing, so `many (pure x)` fails to compile
 -- rather than hanging. A lexer built on grip would need no fuel here.
-private def go (table : Array (List Char × String)) (acc : List Tok) :
-    Nat → List Char → Except String (List Tok)
+private
+def go
+    (table : Array (List Char × String))
+    (acc : List Tok)
+    : Nat →        -- fuel, seeded at input length
+      List Char →  -- remaining characters to lex
+      Except String (List Tok)
   | _, [] => .ok acc.reverse
   | 0, _ => .error "lexer made no progress"
   | fuel + 1, c :: cs =>
@@ -140,7 +159,10 @@ private def go (table : Array (List Char × String)) (acc : List Tok) :
 /-- `mod` is the only word-shaped operator Rodin treats as infix; the rest of the word
 operators (`card`, `dom`, `bool`, ...) are ordinary identifiers applied to an argument,
 so the lexer leaves them alone. -/
-def lex (s : String) : Except EventB.Error (List Tok) :=
+def lex
+    (s : String)
+    : Except EventB.Error (List Tok)
+    :=
   let cs := s.toList
   (go operatorTable [] cs.length cs).mapError EventB.Error.formula