diff --git a/OATP/Artifacts.lean b/OATP/Artifacts.lean
index 0a5460b..862eb92 100644
--- a/OATP/Artifacts.lean
+++ b/OATP/Artifacts.lean
@@ -21,17 +21,28 @@ structure Run where
   directory : System.FilePath
   deriving Repr
 
-private def safeName (value : String) : String :=
+private
+def safeName
+    (value : String)
+    : String
+    :=
   let name := String.ofList <| value.toList.map fun character =>
     if character.isAlphanum || character == '-' || character == '_' then character else '_'
   if name.isEmpty then "run" else name
 
-private def roots : IO (List System.FilePath) := do
+private
+def roots
+    : IO (List System.FilePath)
+    := do
   let current ← IO.currentDir
   let fallback ← OATP.Config.directory
   pure <| System.FilePath.join current ".oatp" :: fallback.toList
 
-def start (label : String) (problem : Problem) : IO (Option Run) := do
+def start
+    (label : String)
+    (problem : Problem)
+    : IO (Option Run)
+    := do
   let stamp ← IO.monoMsNow
   for root in ← roots do
     -- ponytail: 64 bounded suffixes cover same-millisecond concurrent runs;
@@ -48,11 +59,19 @@ def start (label : String) (problem : Problem) : IO (Option Run) := do
       catch _ => pure ()
   pure none
 
-def write (run : Run) (name content : String) : IO Unit := do
+def write
+    (run : Run)
+    (name content : String)
+    : IO Unit
+    := do
   try IO.FS.writeFile (System.FilePath.join run.directory name) content
   catch _ => pure ()
 
-def writeCommand (run : Run) (command : String) : IO Unit :=
+def writeCommand
+    (run : Run)
+    (command : String)
+    : IO Unit
+    :=
   write run "command.txt" command
 
 end OATP.Artifacts
diff --git a/OATP/Config.lean b/OATP/Config.lean
index b00257f..16aa317 100644
--- a/OATP/Config.lean
+++ b/OATP/Config.lean
@@ -21,7 +21,10 @@ structure Preferences where
 
 def default : Preferences := {}
 
-private def configRoot : IO (Option System.FilePath) := do
+private
+def configRoot
+    : IO (Option System.FilePath)
+    := do
   match ← IO.getEnv "XDG_CONFIG_HOME" with
   | some path => pure (some ⟨path⟩)
   | none =>
@@ -29,20 +32,34 @@ private def configRoot : IO (Option System.FilePath) := do
       | some path => pure (some (System.FilePath.join ⟨path⟩ ".config"))
       | none => pure none
 
-def directory : IO (Option System.FilePath) := do
+def directory
+    : IO (Option System.FilePath)
+    := do
   pure <| (← configRoot).map fun root => System.FilePath.join root "oatp"
 
-def path : IO (Option System.FilePath) := do
+def path
+    : IO (Option System.FilePath)
+    := do
   pure <| (← directory).map fun root => System.FilePath.join root "config.json"
 
 private def field (json : Json) (name : String) : Option Json := json.get? name
 
-private def stringField (json : Json) (name fallback : String) : String :=
+private
+def stringField
+    (json : Json)
+    (name fallback : String)
+    : String
+    :=
   match field json name with
   | some (.str value) => value
   | _ => fallback
 
-private def stringArrayField (json : Json) (name : String) : Array String :=
+private
+def stringArrayField
+    (json : Json)
+    (name : String)
+    : Array String
+    :=
   match field json name with
   | some (.arr values) =>
       let result : List String := values.toList.filterMap fun value =>
@@ -52,7 +69,10 @@ private def stringArrayField (json : Json) (name : String) : Array String :=
       result.toArray
   | _ => #[]
 
-private def fromJson : Json → Preferences
+private
+def fromJson
+    : Json →
+      Preferences
   | json => {
       theory := stringField json "theory" default.theory
       defaultProver := stringField json "defaultProver" default.defaultProver
@@ -64,7 +84,11 @@ private def fromJson : Json → Preferences
       theme := stringField json "theme" default.theme
     }
 
-private def toJson (preferences : Preferences) : Json :=
+private
+def toJson
+    (preferences : Preferences)
+    : Json
+    :=
   .obj #[
     ("theory", .str preferences.theory),
     ("defaultProver", .str preferences.defaultProver),
@@ -74,7 +98,9 @@ private def toJson (preferences : Preferences) : Json :=
     ("theme", .str preferences.theme)
   ]
 
-def load : IO (Preferences × Option String) := do
+def load
+    : IO (Preferences × Option String)
+    := do
   match ← path with
   | none => pure (default, none)
   | some file =>
@@ -85,7 +111,10 @@ def load : IO (Preferences × Option String) := do
         | .error _ => pure (default, some s!"invalid config `{file}`: expected a JSON object")
       catch _ => pure (default, none)
 
-def save (preferences : Preferences) : IO (Option String) := do
+def save
+    (preferences : Preferences)
+    : IO (Option String)
+    := do
   match ← path with
   | none => pure (some "cannot persist preferences: HOME/XDG_CONFIG_HOME is unset")
   | some file =>
diff --git a/OATP/Core.lean b/OATP/Core.lean
index e901550..66b94b7 100644
--- a/OATP/Core.lean
+++ b/OATP/Core.lean
@@ -25,11 +25,15 @@ inductive RunStrategy where
 
 namespace RunStrategy
 
-def name : RunStrategy → String
+def name
+    : RunStrategy →
+      String
   | .all => "all"
   | .firstSuccess => "first-success"
 
-def ofString : String → Option RunStrategy
+def ofString
+    : String →
+      Option RunStrategy
   | "all" => some .all
   | "first-success" => some .firstSuccess
   | _ => none
@@ -45,7 +49,10 @@ structure Prover where
 
 namespace Prover
 
-def label (prover : Prover) : String :=
+def label
+    (prover : Prover)
+    : String
+    :=
   match prover.version with
   | some version => s!"{prover.name} {version}"
   | none => prover.name
@@ -67,7 +74,10 @@ namespace SZSStatus
 
 private def statusPrefixes : List String := ["% SZS status ", "# SZS status "]
 
-def tokenFromLine (line : String) : Option String :=
+def tokenFromLine
+    (line : String)
+    : Option String
+    :=
   let line := line.trimAscii.toString
   let rec find : List String → Option String
     | [] => none
@@ -78,11 +88,18 @@ def tokenFromLine (line : String) : Option String :=
         else find markers
   find statusPrefixes
 
-private def tokenFromLines : List String → Option String
+private
+def tokenFromLines
+    : List String →
+      Option String
   | [] => none
   | line :: lines => tokenFromLine line |>.orElse (fun _ => tokenFromLines lines)
 
-private def resultTokenFromLine (line : String) : Option String :=
+private
+def resultTokenFromLine
+    (line : String)
+    : Option String
+    :=
   let line := line.trimAscii.toString
   match line.splitOn " says " with
   | _ :: result :: _ =>
@@ -90,12 +107,17 @@ private def resultTokenFromLine (line : String) : Option String :=
       if token.isEmpty then none else some token
   | _ => none
 
-def tokenFromOutput (output : String) : Option String :=
+def tokenFromOutput
+    (output : String)
+    : Option String
+    :=
   let lines := output.splitOn "\n"
   tokenFromLines lines |>.orElse fun _ =>
     lines.findSome? resultTokenFromLine
 
-def ofString : String → Option SZSStatus
+def ofString
+    : String →
+      Option SZSStatus
   | "Theorem" | "theorem" => some .theorem
   | "Unsatisfiable" | "unsatisfiable" => some .unsatisfiable
   | "Satisfiable" | "satisfiable" => some .satisfiable
@@ -107,10 +129,15 @@ def ofString : String → Option SZSStatus
   | "Unknown" | "unknown" => some .unknown
   | _ => none
 
-def ofOutput (output : String) : Option SZSStatus :=
+def ofOutput
+    (output : String)
+    : Option SZSStatus
+    :=
   tokenFromOutput output >>= ofString
 
-def toString : SZSStatus → String
+def toString
+    : SZSStatus →
+      String
   | .theorem => "Theorem"
   | .unsatisfiable => "Unsatisfiable"
   | .satisfiable => "Satisfiable"
@@ -120,11 +147,15 @@ def toString : SZSStatus → String
   | .error => "Error"
   | .unknown => "Unknown"
 
-def isSuccess : SZSStatus → Bool
+def isSuccess
+    : SZSStatus →
+      Bool
   | .theorem | .unsatisfiable => true
   | _ => false
 
-instance : ToString SZSStatus where
+instance
+    : ToString SZSStatus
+    where
   toString := toString
 
 end SZSStatus
@@ -155,12 +186,16 @@ inductive Outcome where
   | failed (message : String) (artifact : Option Artifact := none)
   deriving Repr
 
-def Outcome.artifact : Outcome → Option Artifact
+def Outcome.artifact
+    : Outcome →
+      Option Artifact
   | .candidate artifact => some artifact
   | .timedOut artifact => some artifact
   | .failed _ artifact => artifact
 
-def Outcome.status : Outcome → String
+def Outcome.status
+    : Outcome →
+      String
   | .candidate artifact => s!"candidate ({artifact.status})"
   | .timedOut _ => "timeout"
   | .failed message _ => s!"failed: {message}"
diff --git a/OATP/Http.lean b/OATP/Http.lean
index 779ad50..8825bfe 100644
--- a/OATP/Http.lean
+++ b/OATP/Http.lean
@@ -26,29 +26,46 @@ structure Field where
   value : String
   deriving BEq, DecidableEq, Repr
 
-private def hexDigits : Array Char :=
+private
+def hexDigits
+    : Array Char
+    :=
   #[
     '0', '1', '2', '3', '4', '5', '6', '7',
     '8', '9', 'A', 'B', 'C', 'D', 'E', 'F'
   ]
 
-private def isUnreserved (byte : UInt8) : Bool :=
+private
+def isUnreserved
+    (byte : UInt8)
+    : Bool
+    :=
   (byte >= 48 && byte <= 57) ||
   (byte >= 65 && byte <= 90) ||
   (byte >= 97 && byte <= 122) ||
   byte == 45 || byte == 46 || byte == 95 || byte == 126
 
-private def encodeByte (byte : UInt8) : String :=
+private
+def encodeByte
+    (byte : UInt8)
+    : String
+    :=
   if isUnreserved byte then
     Char.ofNat byte.toNat |>.toString
   else
     let n := byte.toNat
     s!"%{hexDigits[n / 16]!}{hexDigits[n % 16]!}"
 
-def encodeComponent (value : String) : String :=
+def encodeComponent
+    (value : String)
+    : String
+    :=
   String.join (value.toUTF8.toList.map encodeByte)
 
-def encodeUrlEncoded (fields : Array Field) : String :=
+def encodeUrlEncoded
+    (fields : Array Field)
+    : String
+    :=
   String.intercalate "&" <| fields.toList.map fun field =>
     s!"{encodeComponent field.name}={encodeComponent field.value}"
 
@@ -59,11 +76,19 @@ structure MultipartPart where
   contentType : Option String := none
   deriving BEq, DecidableEq, Repr
 
-private def validHeaderValue (value : String) : Bool :=
+private
+def validHeaderValue
+    (value : String)
+    : Bool
+    :=
   value.toList.all fun character =>
     character != '"' && character != '\\' && character != '\r' && character != '\n'
 
-def encodeMultipart (boundary : String) (parts : Array MultipartPart) : Except String String := do
+def encodeMultipart
+    (boundary : String)
+    (parts : Array MultipartPart)
+    : Except String String
+    := do
   if boundary.isEmpty || !boundary.toList.all (fun character =>
       character.isAlphanum || character == '-' || character == '_') then
     throw "multipart boundary must contain only letters, digits, '-' or '_'"
@@ -95,7 +120,9 @@ inductive Method where
   | post
   deriving BEq, DecidableEq, Repr
 
-def Method.toString : Method → String
+def Method.toString
+    : Method →
+      String
   | .get => "GET"
   | .post => "POST"
 
@@ -115,7 +142,10 @@ structure Response where
   stderr : String := ""
   deriving Repr
 
-def commandVersion (command : String) : IO (Option String) := do
+def commandVersion
+    (command : String)
+    : IO (Option String)
+    := do
   try
     let output ← IO.Process.output { cmd := command, args := #["--version"] }
     if output.exitCode != 0 then
@@ -126,7 +156,9 @@ def commandVersion (command : String) : IO (Option String) := do
       pure <| if line.isEmpty then none else some line
   catch _ => pure none
 
-def availableTransports : IO (Array String) := do
+def availableTransports
+    : IO (Array String)
+    := do
   let mut available := #[]
   for command in #["curl", "wget"] do
     if (← commandVersion command).isSome then
@@ -142,7 +174,9 @@ inductive Error where
   | bodyTooLarge (actual limit : Nat)
   deriving Repr
 
-def Error.message : Error → String
+def Error.message
+    : Error →
+      String
   | .io message => s!"HTTP IO failed: {message}"
   | .invalidRequest message => s!"invalid HTTP request: {message}"
   | .transport message => s!"HTTP transport failed: {message}"
@@ -158,7 +192,11 @@ inductive Transport where
 
 def statusMarker := "OATP_HTTP_STATUS:"
 
-private def statusFromOutput (output : String) : Option (String × Nat) :=
+private
+def statusFromOutput
+    (output : String)
+    : Option (String × Nat)
+    :=
   let parts := output.splitOn statusMarker
   match parts.reverse with
   | code :: before :: _ =>
@@ -167,7 +205,11 @@ private def statusFromOutput (output : String) : Option (String × Nat) :=
       | none => none
   | _ => none
 
-private def requestWithCurlUnsafe (request : Request) : IO (Except Error Response) := do
+private
+def requestWithCurlUnsafe
+    (request : Request)
+    : IO (Except Error Response)
+    := do
   let base : Array String := #[
     "--silent", "--show-error",
     "--max-time", toString request.maxSeconds,
@@ -195,13 +237,21 @@ private def requestWithCurlUnsafe (request : Request) : IO (Except Error Respons
       else
         return Except.ok { statusCode := statusCode, body := body, stderr := output.stderr }
 
-private def statusFromWgetLine (line : String) : Option Nat :=
+private
+def statusFromWgetLine
+    (line : String)
+    : Option Nat
+    :=
   let fields := line.trimAscii.toString.splitOn " " |>.filter (!·.isEmpty)
   match fields with
   | _ :: code :: _ => code.toNat?
   | _ => none
 
-private def statusFromWgetOutput (output : String) : Option Nat :=
+private
+def statusFromWgetOutput
+    (output : String)
+    : Option Nat
+    :=
   let rec find : List String → Option Nat
     | [] => none
     | line :: lines =>
@@ -212,7 +262,11 @@ private def statusFromWgetOutput (output : String) : Option Nat :=
         else find lines
   find (output.splitOn "\n")
 
-private def requestWithWgetUnsafe (request : Request) : IO (Except Error Response) := do
+private
+def requestWithWgetUnsafe
+    (request : Request)
+    : IO (Except Error Response)
+    := do
   let base : Array String := #[
     "--quiet", "--server-response", "--max-redirect=0", "--tries=1",
     "--timeout=" ++ toString request.maxSeconds,
@@ -238,7 +292,11 @@ private def requestWithWgetUnsafe (request : Request) : IO (Except Error Respons
       else
         return Except.ok { statusCode, body := output.stdout }
 
-private def validateRequest (request : Request) : Except Error Unit := do
+private
+def validateRequest
+    (request : Request)
+    : Except Error Unit
+    := do
   if request.url.isEmpty then
     throw (.invalidRequest "HTTP request URL must not be empty")
   if request.maxSeconds == 0 then
@@ -249,7 +307,11 @@ private def validateRequest (request : Request) : Except Error Unit := do
   if actual > request.maxRequestBodyBytes then
     throw (.requestBodyTooLarge actual request.maxRequestBodyBytes)
 
-private def requestWithTransportUnsafe (request : Request) : IO (Except Error Response) := do
+private
+def requestWithTransportUnsafe
+    (request : Request)
+    : IO (Except Error Response)
+    := do
   match validateRequest request with
   | .error error => return .error error
   | .ok _ => pure ()
@@ -261,13 +323,20 @@ private def requestWithTransportUnsafe (request : Request) : IO (Except Error Re
   else
     pure <| Except.error (.transport "OATP requires curl or wget for HTTPS transport")
 
-def requestWithTransport (request : Request) : IO (Except Error Response) := do
+def requestWithTransport
+    (request : Request)
+    : IO (Except Error Response)
+    := do
   try
     requestWithTransportUnsafe request
   catch error =>
     pure (.error (.io s!"{error}"))
 
-def requestWith (transport : Transport) (request : Request) : IO (Except Error Response) := do
+def requestWith
+    (transport : Transport)
+    (request : Request)
+    : IO (Except Error Response)
+    := do
   try
     match validateRequest request with
     | .error error => pure (.error error)
@@ -278,7 +347,10 @@ def requestWith (transport : Transport) (request : Request) : IO (Except Error R
   catch error =>
     pure (.error (.io s!"{error}"))
 
-def requestWithCurl (request : Request) : IO (Except Error Response) := do
+def requestWithCurl
+    (request : Request)
+    : IO (Except Error Response)
+    := do
   requestWith .curl request
 
 end OATP.Http
diff --git a/OATP/Lean.lean b/OATP/Lean.lean
index d39cea9..fc4ce30 100644
--- a/OATP/Lean.lean
+++ b/OATP/Lean.lean
@@ -24,7 +24,11 @@ structure CheckedProof where
   proof : Expr
   target : Expr
 
-private def prettyExpr (expression : Expr) : MetaM String := do
+private
+def prettyExpr
+    (expression : Expr)
+    : MetaM String
+    := do
   let formatted ← ppExpr expression
   pure s!"{formatted}"
 
@@ -41,7 +45,11 @@ def snapshot (mvarId : MVarId) : MetaM GoalSnapshot := mvarId.withContext do
     target := ← prettyExpr target
   }
 
-def check (mvarId : MVarId) (candidate : Expr) : MetaM (Except String CheckedProof) :=
+def check
+    (mvarId : MVarId)
+    (candidate : Expr)
+    : MetaM (Except String CheckedProof)
+    :=
   mvarId.withContext do
   let target ← instantiateMVars (← mvarId.getType)
   let candidate ← instantiateMVars candidate
@@ -53,8 +61,11 @@ def check (mvarId : MVarId) (candidate : Expr) : MetaM (Except String CheckedPro
     let actual ← prettyExpr candidateType
     pure (.error s!"candidate type mismatch: expected {expected}, got {actual}")
 
-def checkAndAssign (mvarId : MVarId) (candidate : Expr) :
-    MetaM (Except String CheckedProof) := mvarId.withContext do
+def checkAndAssign
+    (mvarId : MVarId)
+    (candidate : Expr)
+    : MetaM (Except String CheckedProof)
+    := mvarId.withContext do
   match ← check mvarId candidate with
   | .error message => pure (.error message)
   | .ok checked =>
diff --git a/OATP/Lean/Repl.lean b/OATP/Lean/Repl.lean
index e0e32fa..d0e72ad 100644
--- a/OATP/Lean/Repl.lean
+++ b/OATP/Lean/Repl.lean
@@ -47,7 +47,9 @@ private def coreContext : Core.Context := {
   quotContext := `OATP
 }
 
-def create : IO Runtime := do
+def create
+    : IO Runtime
+    := do
   Lean.initSearchPath (← Lean.getBuildDir)
   let env ← Lean.importModules #[{ module := `Init.Prelude }] {}
   pure {
@@ -56,22 +58,42 @@ def create : IO Runtime := do
     metaState := {}
   }
 
-private def runMeta {α : Type} (runtime : Runtime) (action : MetaM α) :
-    IO (α × Runtime) := do
+private
+def runMeta
+    {α : Type}
+    (runtime : Runtime)
+    (action : MetaM α)
+    : IO (α × Runtime)
+    := do
   let (value, coreState, metaState) ← action.toIO runtime.coreContext runtime.coreState {}
     runtime.metaState
   pure (value, { runtime with coreState, metaState })
 
-private def addAtom (atoms : Array String) (name : String) : Array String :=
+private
+def addAtom
+    (atoms : Array String)
+    (name : String)
+    : Array String
+    :=
   if atoms.contains name then atoms else atoms.push name
 
 private abbrev TranslationM := ExceptT String MetaM
 
-private def translationError {α : Type} (message : String) : TranslationM α :=
+private
+def translationError
+    {α : Type}
+    (message : String)
+    : TranslationM α
+    :=
   ExceptT.mk (pure (.error message))
 
-private partial def atomNames (formula : _root_.TPTP.Formula.Expr) (atoms : Array String) :
-    Array String :=
+private
+partial
+def atomNames
+    (formula : _root_.TPTP.Formula.Expr)
+    (atoms : Array String)
+    : Array String
+    :=
   match formula with
   | .atom predicate arguments =>
       if arguments.isEmpty then addAtom atoms predicate else atoms
@@ -81,19 +103,34 @@ private partial def atomNames (formula : _root_.TPTP.Formula.Expr) (atoms : Arra
       atomNames right (atomNames left atoms)
   | .forall _ body | .exists _ body => atomNames body atoms
 
-private def withAtoms {α : Type} (atoms : List String)
-    (action : Array (String × Expr) → TranslationM α) : MetaM (Except String α) :=
+private
+def withAtoms
+    {α : Type}
+    (atoms : List String)
+    (action : Array (String × Expr) → TranslationM α)
+    : MetaM (Except String α)
+    :=
   match atoms with
   | [] => (action #[]).run
   | atom :: rest =>
     withLocalDeclD (Name.mkSimple atom) (mkSort .zero) fun fvar =>
       withAtoms rest fun locals => action (locals.push (atom, fvar))
 
-private def lookupAtom (atoms : Array (String × Expr)) (name : String) : Option Expr :=
+private
+def lookupAtom
+    (atoms : Array (String × Expr))
+    (name : String)
+    : Option Expr
+    :=
   atoms.find? (·.1 == name) |>.map Prod.snd
 
-private partial def toLean (atoms : Array (String × Expr))
-    (formula : _root_.TPTP.Formula.Expr) : TranslationM Expr := do
+private
+partial
+def toLean
+    (atoms : Array (String × Expr))
+    (formula : _root_.TPTP.Formula.Expr)
+    : TranslationM Expr
+    := do
   match formula with
   | .atom predicate arguments =>
       if !arguments.isEmpty then
@@ -123,33 +160,51 @@ where
     let right ← toLean atoms right
     ExceptT.lift <| mkAppM name #[left, right]
 
-private def makeGoal (source : String) (formula : _root_.TPTP.Formula.Expr) :
-    MetaM (Except String Goal) := do
+private
+def makeGoal
+    (source : String)
+    (formula : _root_.TPTP.Formula.Expr)
+    : MetaM (Except String Goal)
+    := do
   let atoms := atomNames formula #[]
   withAtoms atoms.toList fun locals => do
     let target ← toLean locals formula
     let goal ← ExceptT.lift <| mkFreshExprMVar (some target)
     pure { mvarId := goal.mvarId!, source, atoms }
 
-def goalFromFormula (runtime : Runtime) (source : String) :
-    IO (Except String (Runtime × Goal)) := do
+def goalFromFormula
+    (runtime : Runtime)
+    (source : String)
+    : IO (Except String (Runtime × Goal))
+    := do
   match OATP.TPTP.Syntax.parseFormula source with
   | .error error => pure (.error (error.pretty source.toUTF8))
   | .ok formula =>
       let (result, runtime) ← runMeta runtime (makeGoal source formula)
       pure <| result.map fun goal => (runtime, goal)
 
-def snapshot (runtime : Runtime) (goal : Goal) : IO (Runtime × OATP.GoalSnapshot) := do
+def snapshot
+    (runtime : Runtime)
+    (goal : Goal)
+    : IO (Runtime × OATP.GoalSnapshot)
+    := do
   let (value, runtime) ← runMeta runtime (OATP.Lean.snapshot goal.mvarId)
   pure (runtime, value)
 
-def translateToTPTP (runtime : Runtime) (goal : Goal) :
-    IO (Runtime × Except String OATP.Lean.GoalTranslation) := do
+def translateToTPTP
+    (runtime : Runtime)
+    (goal : Goal)
+    : IO (Runtime × Except String OATP.Lean.GoalTranslation)
+    := do
   let (value, runtime) ← runMeta runtime (OATP.Lean.translateGoal goal.mvarId)
   pure (runtime, value)
 
-def reconstruct (runtime : Runtime) (goal : Goal) (step : OATP.Proof.Step) :
-    IO (Runtime × Except String RenderedTerm) := do
+def reconstruct
+    (runtime : Runtime)
+    (goal : Goal)
+    (step : OATP.Proof.Step)
+    : IO (Runtime × Except String RenderedTerm)
+    := do
   let action : MetaM (Except String RenderedTerm) := do
     match ← OATP.Proof.reconstruct goal.mvarId step with
     | .error message => pure (.error message)
diff --git a/OATP/Portfolio.lean b/OATP/Portfolio.lean
index 6adf772..e46a99c 100644
--- a/OATP/Portfolio.lean
+++ b/OATP/Portfolio.lean
@@ -40,13 +40,19 @@ inductive Result where
   | failed (attempt : Attempt) (failure : Failure)
   deriving Repr
 
-private def responseErrorMessage : SystemOnTPTP.ResponseError → String
+private
+def responseErrorMessage
+    : SystemOnTPTP.ResponseError →
+      String
   | .httpStatus status => s!"SystemOnTPTP returned HTTP {status}"
   | .missingStatus => "SystemOnTPTP response did not contain an SZS status"
   | .unsupportedStatus status => s!"SystemOnTPTP returned unsupported SZS status `{status}`"
   | .malformedBody message => s!"SystemOnTPTP response was not valid HTML: {message}"
 
-private def httpErrorMessage : Http.Error → String
+private
+def httpErrorMessage
+    : Http.Error →
+      String
   | .io message => s!"HTTP IO failed: {message}"
   | .invalidRequest message => s!"invalid HTTP request: {message}"
   | .transport message => s!"HTTP transport failed: {message}"
@@ -54,17 +60,25 @@ private def httpErrorMessage : Http.Error → String
   | .requestBodyTooLarge actual limit => s!"HTTP request exceeded {limit} bytes ({actual} captured)"
   | .bodyTooLarge actual limit => s!"HTTP response exceeded {limit} bytes ({actual} captured)"
 
-def Failure.message : Failure → String
+def Failure.message
+    : Failure →
+      String
   | .process message => message
   | .http error => httpErrorMessage error
   | .response error _ => responseErrorMessage error
 
-def Failure.output : Failure → String
+def Failure.output
+    : Failure →
+      String
   | .http (.malformedStatus output) => output
   | .process _ | .http _ => ""
   | .response _ output => output
 
-def execute (problem : Problem) (attempt : Attempt) : IO Result := do
+def execute
+    (problem : Problem)
+    (attempt : Attempt)
+    : IO Result
+    := do
   match attempt.backend with
   | .local command =>
       match ← Process.run { name := attempt.name } problem attempt.limits command with
@@ -87,8 +101,14 @@ def execute (problem : Problem) (attempt : Attempt) : IO Result := do
               pure (.failed attempt (.response error output))
 
 -- partiality: task completion is external and waitAny' controls progress through the pending set.
-private partial def collect (pending : List (Task (Except IO.Error Result)))
-    (results : Array Result) (onResult : Result → IO Unit) : IO (Array Result) := do
+private
+partial
+def collect
+    (pending : List (Task (Except IO.Error Result)))
+    (results : Array Result)
+    (onResult : Result → IO Unit)
+    : IO (Array Result)
+    := do
   match pending with
   | [] => pure results
   | task :: rest =>
@@ -97,21 +117,38 @@ private partial def collect (pending : List (Task (Except IO.Error Result)))
       onResult result
       collect remaining (results.push result) onResult
 
-def runWith (problem : Problem) (attempts : Array Attempt)
-    (onResult : Result → IO Unit := fun _ => pure ()) : IO (Array Result) := do
+def runWith
+    (problem : Problem)
+    (attempts : Array Attempt)
+    (onResult : Result → IO Unit := fun _ => pure ())
+    : IO (Array Result)
+    := do
   let tasks ← attempts.toList.mapM fun attempt =>
     IO.asTask (execute problem attempt) Task.Priority.dedicated
   collect tasks #[] onResult
 
-def run (problem : Problem) (attempts : Array Attempt) : IO (Array Result) :=
+def run
+    (problem : Problem)
+    (attempts : Array Attempt)
+    : IO (Array Result)
+    :=
   runWith problem attempts
 
-private def successful : Result → Bool
+private
+def successful
+    : Result →
+      Bool
   | .artifact _ artifact => SZSStatus.isSuccess artifact.status
   | .failed _ _ => false
 
-private def runUntilSuccess (problem : Problem) (attempts : List Attempt)
-    (results : Array Result) (onResult : Result → IO Unit) : IO (Array Result) := do
+private
+def runUntilSuccess
+    (problem : Problem)
+    (attempts : List Attempt)
+    (results : Array Result)
+    (onResult : Result → IO Unit)
+    : IO (Array Result)
+    := do
   match attempts with
   | [] => pure results
   | attempt :: rest =>
@@ -120,8 +157,13 @@ private def runUntilSuccess (problem : Problem) (attempts : List Attempt)
       if successful result then pure (results.push result)
       else runUntilSuccess problem rest (results.push result) onResult
 
-def runWithStrategy (problem : Problem) (attempts : Array Attempt) (strategy : RunStrategy)
-    (onResult : Result → IO Unit := fun _ => pure ()) : IO (Array Result) :=
+def runWithStrategy
+    (problem : Problem)
+    (attempts : Array Attempt)
+    (strategy : RunStrategy)
+    (onResult : Result → IO Unit := fun _ => pure ())
+    : IO (Array Result)
+    :=
   match strategy with
   | .all => runWith problem attempts onResult
   | .firstSuccess => runUntilSuccess problem attempts.toList #[] onResult
diff --git a/OATP/Process.lean b/OATP/Process.lean
index d007ec4..3727438 100644
--- a/OATP/Process.lean
+++ b/OATP/Process.lean
@@ -24,7 +24,10 @@ structure Command where
   deriving BEq, DecidableEq, Repr
 
 /-- Add the stdin filename expected by local provers that require one. -/
-def Command.withStdinProblem (command : Command) : Command :=
+def Command.withStdinProblem
+    (command : Command)
+    : Command
+    :=
   let executable := (command.executable.splitOn "/").getLast?.getD command.executable
   if executable == "metis" && !command.arguments.any (· == "-") then
     { command with arguments := command.arguments.push "-" }
@@ -37,8 +40,14 @@ inductive Error where
 
 -- partiality: process completion and the monotonic clock are external; the deadline bounds
 -- polling behavior, not kernel recursion.
-private partial def waitForExit {cfg : IO.Process.StdioConfig}
-    (child : IO.Process.Child cfg) (deadline : Nat) : IO (Bool × UInt32) := do
+private
+partial
+def waitForExit
+    {cfg : IO.Process.StdioConfig}
+    (child : IO.Process.Child cfg)
+    (deadline : Nat)
+    : IO (Bool × UInt32)
+    := do
   match ← child.tryWait with
   | some exitCode => pure (false, exitCode)
   | none =>
@@ -52,8 +61,14 @@ private partial def waitForExit {cfg : IO.Process.StdioConfig}
         IO.sleep (min 10 remaining).toUInt32
         waitForExit child deadline
 
-private def runUnsafe (prover : Prover) (problem : Problem) (limits : Limits) (command : Command) :
-    IO (Except Error Artifact) := do
+private
+def runUnsafe
+    (prover : Prover)
+    (problem : Problem)
+    (limits : Limits)
+    (command : Command)
+    : IO (Except Error Artifact)
+    := do
   let command := command.withStdinProblem
   let artifacts ← OATP.Artifacts.start s!"local {command.executable}" problem
   for run in artifacts do
@@ -119,8 +134,13 @@ private def runUnsafe (prover : Prover) (problem : Problem) (limits : Limits) (c
     OATP.Artifacts.write run "result.txt" s!"{status}\n"
   return .ok artifact
 
-def run (prover : Prover) (problem : Problem) (limits : Limits) (command : Command) :
-    IO (Except Error Artifact) := do
+def run
+    (prover : Prover)
+    (problem : Problem)
+    (limits : Limits)
+    (command : Command)
+    : IO (Except Error Artifact)
+    := do
   try
     runUnsafe prover problem limits command
   catch error =>
diff --git a/OATP/Proof.lean b/OATP/Proof.lean
index 57176cc..fcb368b 100644
--- a/OATP/Proof.lean
+++ b/OATP/Proof.lean
@@ -29,16 +29,27 @@ inductive Step where
   | implicationIntro (localName : Name) (body : Step)
   deriving Repr
 
-def stepNames : List String :=
+def stepNames
+    : List String
+    :=
   ["true-intro", "exact", "and-left", "and-right", "and-intro", "implication-intro"]
 
-private def andParts (target : Expr) : MetaM (Option (Expr × Expr)) := do
+private
+def andParts
+    (target : Expr)
+    : MetaM (Option (Expr × Expr))
+    := do
   match ← whnf target with
   | .app (.app (.const ``And _) left) right => pure (some (left, right))
   | _ => pure none
 
-private def projection (target : Expr) (localName : Name) (useLeft : Bool) :
-    MetaM (Except String Expr) := do
+private
+def projection
+    (target : Expr)
+    (localName : Name)
+    (useLeft : Bool)
+    : MetaM (Except String Expr)
+    := do
   let hypothesis ← getFVarFromUserName localName
   match ← andParts (← inferType hypothesis) with
   | none => pure (.error s!"local hypothesis `{localName}` is not a conjunction")
@@ -50,7 +61,11 @@ private def projection (target : Expr) (localName : Name) (useLeft : Bool) :
       else
         pure (.error s!"conjunction projection from `{localName}` has the wrong target")
 
-private def build (target : Expr) : Step → MetaM (Except String Expr)
+private
+def build
+    (target : Expr)
+    : Step →
+      MetaM (Except String Expr)
   | .exact localName => do
       let hypothesis ← getFVarFromUserName localName
       let hypothesisType ← inferType hypothesis
@@ -82,8 +97,11 @@ private def build (target : Expr) : Step → MetaM (Except String Expr)
             | .ok proof => pure (.ok (← mkLambdaFVars #[localVar] proof))
       | _ => pure (.error "implication-intro requires an implication target")
 
-def reconstruct (mvarId : MVarId) (step : Step) :
-    MetaM (Except String OATP.Lean.CheckedProof) := mvarId.withContext do
+def reconstruct
+    (mvarId : MVarId)
+    (step : Step)
+    : MetaM (Except String OATP.Lean.CheckedProof)
+    := mvarId.withContext do
   let target ← instantiateMVars (← mvarId.getType)
   match ← build target step with
   | .error message => pure (.error message)
diff --git a/OATP/Properties/Basic.lean b/OATP/Properties/Basic.lean
index 3479d9b..94995fe 100644
--- a/OATP/Properties/Basic.lean
+++ b/OATP/Properties/Basic.lean
@@ -13,11 +13,14 @@ namespace OATP.Properties
 
 open OATP OATP.TPTP
 
-theorem empty_plain_render : OATP.Term.renderPlain #[] = "" := by
+theorem empty_plain_render
+    : OATP.Term.renderPlain #[] = ""
+    := by
   rfl
 
-theorem note_plain_render :
-    OATP.Term.renderPlain #[.note "ready"] = "note: ready" := by
+theorem note_plain_render
+    : OATP.Term.renderPlain #[.note "ready"] = "note: ready"
+    := by
   rfl
 
 theorem goal_context_plain_render :
diff --git a/OATP/ProverReference.lean b/OATP/ProverReference.lean
index babaf54..da8ecf9 100644
--- a/OATP/ProverReference.lean
+++ b/OATP/ProverReference.lean
@@ -29,13 +29,22 @@ namespace ProverReference
 
 def fromLocal (name : String) : ProverReference := { name, kind := .local }
 
-def fromOnline (name : String) : ProverReference :=
+def fromOnline
+    (name : String)
+    : ProverReference
+    :=
   { name := OATP.SystemOnTPTP.onlineSystemId name, kind := .online }
 
-def ofString (name : String) : ProverReference :=
+def ofString
+    (name : String)
+    : ProverReference
+    :=
   if OATP.SystemOnTPTP.isOnlineReference name then fromOnline name else fromLocal name
 
-def fromPersisted (value : String) : Option ProverReference :=
+def fromPersisted
+    (value : String)
+    : Option ProverReference
+    :=
   if value.startsWith "local:" then
     let name := value.drop "local:".length |>.toString
     if name.isEmpty then none else some (fromLocal name)
@@ -44,12 +53,18 @@ def fromPersisted (value : String) : Option ProverReference :=
     if name.isEmpty then none else some (fromOnline name)
   else if value.isEmpty then none else some (ofString value)
 
-def persisted (reference : ProverReference) : String :=
+def persisted
+    (reference : ProverReference)
+    : String
+    :=
   match reference.kind with
   | .local => "local:" ++ reference.name
   | .online => "online:" ++ reference.name
 
-def display (reference : ProverReference) : String :=
+def display
+    (reference : ProverReference)
+    : String
+    :=
   match reference.kind with
   | .local => reference.name
   | .online => OATP.SystemOnTPTP.onlineReference reference.name
diff --git a/OATP/Repl.lean b/OATP/Repl.lean
index 019f7fb..8dfeb7a 100644
--- a/OATP/Repl.lean
+++ b/OATP/Repl.lean
@@ -27,7 +27,9 @@ open OATP.TPTP
 open _root_.Argus
 open _root_.Grip
 
-def helpTopics : List String :=
+def helpTopics
+    : List String
+    :=
   ["cnf", "fof", "tff", "lean", "run", "context", "grammar", "roles"]
 
 def grammarTopics : List String := OATP.TPTP.supportedTheories
@@ -36,13 +38,22 @@ def roleFormats : List String := OATP.TPTP.supportedTheories
 
 def runStrategyChoices : List String := OATP.RunStrategy.choices
 
-def completionParam (typeName : String) (values : List String) : Param String :=
+def completionParam
+    (typeName : String)
+    (values : List String)
+    : Param String
+    :=
   Param.named typeName (Param.enum (values.map fun value => (value, value)))
 
-def contextIndexParam : Param Nat :=
+def contextIndexParam
+    : Param Nat
+    :=
   Param.ofParser "INDEX" (GParser.seqR (GParser.optional (GParser.ch '#')) GParser.nat)
 
-def staticCompletionValues (typeName : String) : List String :=
+def staticCompletionValues
+    (typeName : String)
+    : List String
+    :=
   match typeName with
   | "TOPIC" => helpTopics
   | "FORMAT" => roleFormats
@@ -162,27 +173,43 @@ argus_opts SystemsOptions where
   online : Bool := Spec.switch "online" (some 'o') "Also fetch online provers";
   catalogue : OATP.Argus.CatalogueOptions := OATP.Argus.CatalogueOptions.spec
 
-private def parseSpec {α : Type} {g : Grade} (spec : Argus.Spec g α)
-    (args : List String) : Except String α :=
+private
+def parseSpec
+    {α : Type}
+    {g : Grade}
+    (spec : Argus.Spec g α)
+    (args : List String)
+    : Except String α
+    :=
   match Argus.run spec args with
   | .ok value => .ok value
   | .error errors => .error (String.intercalate "\n" (errors.map Argus.Err.message))
 
-private def splitArguments : List String → List String × List String
+private
+def splitArguments
+    : List String →
+      List String × List String
   | [] => ([], [])
   | "__OATP_ARGS__" :: rest => ([], rest)
   | value :: rest =>
       let (before, after) := splitArguments rest
       (value :: before, after)
 
-private def splitTerminator : List String → List String × Option (List String)
+private
+def splitTerminator
+    : List String →
+      List String × Option (List String)
   | [] => ([], none)
   | "--" :: rest => ([], some rest)
   | value :: rest =>
       let (before, after) := splitTerminator rest
       (value :: before, after)
 
-private def runRequestOf (options : RunOptions) : RunRequest :=
+private
+def runRequestOf
+    (options : RunOptions)
+    : RunRequest
+    :=
   let (references, arguments) := splitArguments options.references
   { references := (references ++ options.provers).map ProverReference.ofString
     all := options.all
@@ -193,46 +220,73 @@ private def runRequestOf (options : RunOptions) : RunRequest :=
     maxOutput := options.resources.maxOutput.getD OATP.defaultMaxOutputBytes
     arguments }
 
-private def localRequestOf (options : LocalOptions) : LocalRequest :=
+private
+def localRequestOf
+    (options : LocalOptions)
+    : LocalRequest
+    :=
   let (_, arguments) := splitArguments options.arguments
   { executable := options.executable
     timeout := options.resources.timeout.getD OATP.defaultTimeoutSeconds
     maxOutput := options.resources.maxOutput.getD OATP.defaultMaxOutputBytes
     arguments := if arguments.isEmpty then options.arguments else arguments }
 
-private def onlineRequestOf (options : OnlineOptions) : OnlineRequest :=
+private
+def onlineRequestOf
+    (options : OnlineOptions)
+    : OnlineRequest
+    :=
   { system := options.system
     endpoint := options.remote.endpoint
     timeout := options.remote.resources.timeout.getD OATP.defaultTimeoutSeconds
     maxOutput := options.remote.resources.maxOutput.getD OATP.defaultMaxOutputBytes }
 
-private def systemsRequestOf (options : SystemsOptions) : SystemsRequest :=
+private
+def systemsRequestOf
+    (options : SystemsOptions)
+    : SystemsRequest
+    :=
   { online := options.online, endpoint := options.catalogue.endpoint,
     refresh := options.catalogue.refresh, noCache := options.catalogue.noCache }
 
-def parseRunRequest (args : List String) : Except String RunRequest :=
+def parseRunRequest
+    (args : List String)
+    : Except String RunRequest
+    :=
   let (args, tail) := splitTerminator args
   parseSpec RunOptions.spec args |>.map fun request =>
     { runRequestOf request with arguments := tail.getD (runRequestOf request).arguments }
 
-def parseLocalRequest (args : List String) : Except String LocalRequest :=
+def parseLocalRequest
+    (args : List String)
+    : Except String LocalRequest
+    :=
   let (args, tail) := splitTerminator args
   parseSpec LocalOptions.spec args |>.map fun request =>
     { localRequestOf request with arguments := tail.getD (localRequestOf request).arguments }
 
-def parseOnlineRequest (args : List String) : Except String OnlineRequest :=
+def parseOnlineRequest
+    (args : List String)
+    : Except String OnlineRequest
+    :=
   let (args, tail) := splitTerminator args
   match tail with
   | some (_ :: _) => .error "online commands do not accept arguments after --"
   | _ => parseSpec OnlineOptions.spec args |>.map onlineRequestOf
 
-def parseSystemsRequest (args : List String) : Except String SystemsRequest :=
+def parseSystemsRequest
+    (args : List String)
+    : Except String SystemsRequest
+    :=
   let (args, tail) := splitTerminator args
   match tail with
   | some (_ :: _) => .error "systems does not accept arguments after --"
   | _ => parseSpec SystemsOptions.spec args |>.map systemsRequestOf
 
-def splitWords (source : String) : List String :=
+def splitWords
+    (source : String)
+    : List String
+    :=
   let whitespace (character : Char) : Bool := character.isWhitespace
   let (current, words) := source.toList.foldl (fun (current, words) character =>
     if whitespace character then
@@ -242,13 +296,19 @@ def splitWords (source : String) : List String :=
   let words := if current.isEmpty then words else String.ofList current.reverse :: words
   words.reverse
 
-private def textSpec (name help : String) : Spec (1 * (1 * conditional * flexible)) String :=
+private
+def textSpec
+    (name help : String)
+    : Spec (1 * (1 * conditional * flexible)) String
+    :=
   Spec.map (fun values : List String => String.intercalate " " values)
     (Spec.map2 (fun value values => value :: values)
       (Spec.arg name help (Param.named name Param.str))
       (Spec.many (Spec.arg name help (Param.named name Param.str))))
 
-def commandSpec : Argus.Command Command :=
+def commandSpec
+    : Argus.Command Command
+    :=
   Argus.group "oatp"
     [ Argus.cmd "help" (Spec.map Command.help (Spec.opt (Spec.arg "TOPIC" "Help topic"
         (Param.named "TOPIC" Param.str))))
@@ -338,7 +398,11 @@ def commandSpec : Argus.Command Command :=
     , Argus.cmd "quit" (Spec.const .quit) (description := "Leave the REPL")
     , Argus.cmd "exit" (Spec.const .quit) (description := "Leave the REPL") ]
 
-private def commandArgv (source : String) : List String × Option (List String) :=
+private
+def commandArgv
+    (source : String)
+    : List String × Option (List String)
+    :=
   match splitWords source.trimAscii.toString with
   | command :: args =>
       let command := (command.drop 1).toString
@@ -346,8 +410,12 @@ private def commandArgv (source : String) : List String × Option (List String)
       (command :: args, tail)
   | [] => ([], none)
 
-private def appendCommandArguments (command : Command) (tail : Option (List String)) :
-    Except String Command :=
+private
+def appendCommandArguments
+    (command : Command)
+    (tail : Option (List String))
+    : Except String Command
+    :=
   match tail with
   | none => .ok command
   | some arguments =>
@@ -361,7 +429,10 @@ private def appendCommandArguments (command : Command) (tail : Option (List Stri
           if arguments.isEmpty then .ok command
           else .error "command does not accept arguments after --"
 
-def parseCommandSpec (source : String) : Except String Command :=
+def parseCommandSpec
+    (source : String)
+    : Except String Command
+    :=
   let line := source.trimAscii.toString
   if !line.startsWith "/" then .error "commands start with `/`; try `/help`"
   else
@@ -378,15 +449,22 @@ def parseCommandSpec (source : String) : Except String Command :=
           | [] => ""
         .error (message ++ hint)
 
-private def commandChildren : List (Argus.Command Command) :=
+private
+def commandChildren
+    : List (Argus.Command Command)
+    :=
   match commandSpec.body with
   | .subs children => children
   | .opts _ => []
 
 def commandNames : List String := commandChildren.map (·.name)
 
-private def usageArguments : {g : Grade} → {α : Type} → Spec g α →
-    List (String × Bool × Bool)
+private
+def usageArguments
+    : {g : Grade} →
+      {α : Type} →
+      Spec g α →
+      List (String × Bool × Bool)
   | _, _, .const _ | _, _, .switch _ _ _ | _, _, .flag _ _ _ _ => []
   | _, _, .arg name _ _ => [(name, false, false)]
   | _, _, .ap function argument => usageArguments function ++ usageArguments argument
@@ -396,7 +474,11 @@ private def usageArguments : {g : Grade} → {α : Type} → Spec g α →
   | _, _, .many argument => usageArguments argument |>.map fun (name, _, _) =>
       (name, true, true)
 
-private def usageLine (command : Argus.Command Command) : String :=
+private
+def usageLine
+    (command : Argus.Command Command)
+    : String
+    :=
   let flags := if command.toMeta.flags.isEmpty then "" else " [OPTIONS]"
   let arguments := match command.body with
     | .opts spec => usageArguments spec
@@ -406,26 +488,39 @@ private def usageLine (command : Argus.Command Command) : String :=
     output ++ if optional then " [" ++ value ++ "]" else " " ++ value) ""
   command.name ++ flags ++ arguments
 
-def commandHelpText : String :=
+def commandHelpText
+    : String
+    :=
   String.intercalate "\n" <| ["OATP REPL commands"] ++ commandChildren.map fun command =>
     "  /" ++ usageLine command ++ "  " ++ command.description
 
-def parseCommand (source : String) : Command :=
+def parseCommand
+    (source : String)
+    : Command
+    :=
   let line := source.trimAscii.toString
   match parseCommandSpec line with
   | .ok command => command
   | .error _ => .unknown line
 
-def parseInput (source : String) : Submission :=
+def parseInput
+    (source : String)
+    : Submission
+    :=
   if source.trimAscii.toString.startsWith "/" then
     .command (parseCommand source)
   else
     .source source
 
-def helpText : String :=
+def helpText
+    : String
+    :=
   commandHelpText
 
-private def cnfHelp : String :=
+private
+def cnfHelp
+    : String
+    :=
   String.intercalate "\n" [
     "CNF — clause normal form",
     "statement: cnf(NAME, ROLE, CLAUSE).",
@@ -445,7 +540,10 @@ private def cnfHelp : String :=
     "  /state formulas   /roles cnf   /run --prover eprover"
   ]
 
-private def fofHelp : String :=
+private
+def fofHelp
+    : String
+    :=
   String.intercalate "\n" [
     "FOF — first-order formulas",
     "statement: fof(NAME, ROLE, FORMULA).",
@@ -463,7 +561,10 @@ private def fofHelp : String :=
     "use FOF when the problem needs implication, conjunction, or quantifiers"
   ]
 
-private def tffHelp : String :=
+private
+def tffHelp
+    : String
+    :=
   String.intercalate "\n" [
     "TFF — typed first-order formulas",
     "type:     tff(nat_type, type, nat: $tType).",
@@ -476,7 +577,10 @@ private def tffHelp : String :=
     "TFF is parsed as TPTP input; use /state to inspect collected symbols"
   ]
 
-private def grammarHelp : String :=
+private
+def grammarHelp
+    : String
+    :=
   String.intercalate "\n" [
     "Grammar lookup",
     "/grammar cnf       clause normal form",
@@ -490,7 +594,11 @@ private def grammarHelp : String :=
     "Use /help cnf, /help fof, or /help tff for examples."
   ]
 
-private def roleHelp (topic : Option String) : String :=
+private
+def roleHelp
+    (topic : Option String)
+    : String
+    :=
   let format := topic.getD "all"
   String.intercalate "\n" [
     s!"Roles ({format})",
@@ -511,7 +619,10 @@ private def roleHelp (topic : Option String) : String :=
     s!"Use /grammar {format} for the syntax."
   ]
 
-private def leanHelp : String :=
+private
+def leanHelp
+    : String
+    :=
   String.intercalate "\n" [
     "Lean bridge",
     "1. /goal p => p              create a Lean goal",
@@ -524,7 +635,10 @@ private def leanHelp : String :=
     "example result: fun h => h : _fvar.1 → _fvar.1"
   ]
 
-private def runHelp : String :=
+private
+def runHelp
+    : String
+    :=
   String.intercalate "\n" [
     "Provers",
     "/run                    run the configured or first local prover",
@@ -553,7 +667,10 @@ private def runHelp : String :=
     "  /local vampire -- --mode casc"
   ]
 
-private def contextHelp : String :=
+private
+def contextHelp
+    : String
+    :=
   String.intercalate "\n" [
     "Context drawer",
     "/state [TARGET]            open context or focus a box",
@@ -574,7 +691,11 @@ private def contextHelp : String :=
     "theory: /theory fof|cnf|tff (tf1 alias); provers: /provers; theme: /theme NAME"
   ]
 
-private def commandHelp (command : Argus.Command Command) : String :=
+private
+def commandHelp
+    (command : Argus.Command Command)
+    : String
+    :=
   let details := match command.name with
     | "goal" | "to-lean" | "translate-to-lean" | "snapshot" | "to-tptp" | "reconstruct" | "term" =>
         leanHelp
@@ -587,11 +708,17 @@ private def commandHelp (command : Argus.Command Command) : String :=
   String.intercalate "\n" <| [s!"/{usageLine command}", command.description] ++
     (if details.isEmpty then [] else ["", details])
 
-private def normalizeHelpTopic (topic : String) : String :=
+private
+def normalizeHelpTopic
+    (topic : String)
+    : String
+    :=
   let topic := topic.trimAscii.toString
   if topic.startsWith "/" then topic.drop 1 |>.trimAscii.toString else topic
 
-def helpFor : Option String → String
+def helpFor
+    : Option String →
+      String
   | none => helpText
   | some rawTopic =>
       let topic := normalizeHelpTopic rawTopic
@@ -616,11 +743,19 @@ def helpFor : Option String → String
                   "/help run, /help context"
               ]
 
-private def addFormulaCommand (session : Session) (input name role formula : String) :
-    Except String Session :=
+private
+def addFormulaCommand
+    (session : Session)
+    (input name role formula : String)
+    : Except String Session
+    :=
   parseSource session input s!"fof({name}, {role}, {formula})."
 
-def apply (session : Session) (input : String) : Except String Session :=
+def apply
+    (session : Session)
+    (input : String)
+    : Except String Session
+    :=
   match parseInput input with
   | .source source => parseSource session source source
   | .command command =>
diff --git a/OATP/Repl/Context.lean b/OATP/Repl/Context.lean
index f5d7343..0bbcd18 100644
--- a/OATP/Repl/Context.lean
+++ b/OATP/Repl/Context.lean
@@ -63,11 +63,21 @@ structure Session where
   history : Array HistoryEntry := #[]
   deriving Repr
 
-private def addSymbol (symbols : Array Symbol) (symbol : Symbol) : Array Symbol :=
+private
+def addSymbol
+    (symbols : Array Symbol)
+    (symbol : Symbol)
+    : Array Symbol
+    :=
   if symbols.any (· == symbol) then symbols else symbols.push symbol
 
-private partial def collectTerm (term : _root_.TPTP.Formula.Term) (symbols : Array Symbol) :
-    Array Symbol :=
+private
+partial
+def collectTerm
+    (term : _root_.TPTP.Formula.Term)
+    (symbols : Array Symbol)
+    : Array Symbol
+    :=
   match term with
   | .var name => addSymbol symbols { kind := .variable, name }
   | .constant name => addSymbol symbols { kind := .constant, name }
@@ -75,8 +85,13 @@ private partial def collectTerm (term : _root_.TPTP.Formula.Term) (symbols : Arr
       let symbols := addSymbol symbols { kind := .function, name, arity := arguments.size }
       arguments.foldl (fun symbols term => collectTerm term symbols) symbols
 
-private partial def collectFormula (formula : _root_.TPTP.Formula.Expr)
-    (symbols : Array Symbol) : Array Symbol :=
+private
+partial
+def collectFormula
+    (formula : _root_.TPTP.Formula.Expr)
+    (symbols : Array Symbol)
+    : Array Symbol
+    :=
   match formula with
   | .atom predicate arguments =>
       let symbols := addSymbol symbols
@@ -91,7 +106,12 @@ private partial def collectFormula (formula : _root_.TPTP.Formula.Expr)
         addSymbol symbols { kind := .variable, name }) symbols
       collectFormula body symbols
 
-private def formulaView (id cell : Nat) (statement : _root_.TPTP.Statement) : FormulaView :=
+private
+def formulaView
+    (id cell : Nat)
+    (statement : _root_.TPTP.Statement)
+    : FormulaView
+    :=
   match OATP.TPTP.Statement.parseFormula statement with
   | .ok formula =>
       { id, cell
@@ -111,79 +131,141 @@ private def formulaView (id cell : Nat) (statement : _root_.TPTP.Statement) : Fo
         source := statement.render
         formula := statement.formula }
 
-private def contextItems (nextId cell : Nat) (document : _root_.TPTP.Document) :
-    Array ContextItem × Nat :=
+private
+def contextItems
+    (nextId cell : Nat)
+    (document : _root_.TPTP.Document)
+    : Array ContextItem × Nat
+    :=
   document.items.foldl (fun (items, nextId) item =>
     (items.push { id := nextId, cell, value := item }, nextId + 1)) (#[], nextId)
 
-private def viewsOf (items : Array ContextItem) : Array FormulaView :=
+private
+def viewsOf
+    (items : Array ContextItem)
+    : Array FormulaView
+    :=
   items.foldl (fun views item =>
     match item.value with
     | .statement statement => views.push (formulaView item.id item.cell statement)
     | .include _ => views) #[]
 
-private def symbolsOf (views : Array FormulaView) : Array Symbol :=
+private
+def symbolsOf
+    (views : Array FormulaView)
+    : Array Symbol
+    :=
   views.foldl (fun symbols view => view.symbols.foldl addSymbol symbols) #[]
 
-private def problemSourceOf (items : Array ContextItem) : String :=
+private
+def problemSourceOf
+    (items : Array ContextItem)
+    : String
+    :=
   String.intercalate "\n" (items.toList.map (fun item => item.value.render))
 
-private def rebuildContext (session : Session) : Session :=
+private
+def rebuildContext
+    (session : Session)
+    : Session
+    :=
   let formulas := viewsOf session.context
   { session with
     problemSource := problemSourceOf session.context
     formulas
     symbols := symbolsOf formulas }
 
-private def record (session : Session) (input result : String) : Session :=
+private
+def record
+    (session : Session)
+    (input result : String)
+    : Session
+    :=
   { session with
     nextCell := session.nextCell + 1
     history := session.history.push { cell := session.nextCell, input, result } }
 
-def note (session : Session) (input result : String) : Session :=
+def note
+    (session : Session)
+    (input result : String)
+    : Session
+    :=
   record session input result
 
-def addDocument (session : Session) (input : String) (document : _root_.TPTP.Document) : Session :=
+def addDocument
+    (session : Session)
+    (input : String)
+    (document : _root_.TPTP.Document)
+    : Session
+    :=
   let (items, nextContextId) := contextItems session.nextContextId session.nextCell document
   let session := rebuildContext { session with
     context := session.context ++ items
     nextContextId }
   record session input s!"parsed {viewsOf items |>.size} statement(s)"
 
-def clearContext (session : Session) : Session :=
+def clearContext
+    (session : Session)
+    : Session
+    :=
   rebuildContext { session with context := #[] }
 
-private def validateStatement (statement : _root_.TPTP.Statement) : Except String Unit :=
+private
+def validateStatement
+    (statement : _root_.TPTP.Statement)
+    : Except String Unit
+    :=
   match statement.kind, statement.role with
   | .cnf, .conjecture =>
       .error ("CNF does not support the `conjecture` role; use " ++
         "`negated_conjecture` with a negated clause")
   | _, _ => pure ()
 
-private def validateDocument (document : _root_.TPTP.Document) : Except String Unit :=
+private
+def validateDocument
+    (document : _root_.TPTP.Document)
+    : Except String Unit
+    :=
   document.items.toList.mapM (fun item => match item with
     | _root_.TPTP.Item.statement statement => validateStatement statement
     | _root_.TPTP.Item.include _ => pure ()) |>.map (fun _ => ())
 
-private def parseDocument (source : String) : Except String _root_.TPTP.Document := do
+private
+def parseDocument
+    (source : String)
+    : Except String _root_.TPTP.Document
+    := do
   match OATP.TPTP.parse source with
   | .error error => .error (error.pretty source.toUTF8)
   | .ok document =>
       validateDocument document
       pure document
 
-def parseSource (session : Session) (input source : String) : Except String Session :=
+def parseSource
+    (session : Session)
+    (input source : String)
+    : Except String Session
+    :=
   match parseDocument source with
   | .ok document => pure (addDocument session input document)
   | .error message => .error message
 
 private def contextIndexText (index : Nat) : String := s!"#{index}"
 
-private def missingContextIndices (session : Session) (indices : List Nat) : List Nat :=
+private
+def missingContextIndices
+    (session : Session)
+    (indices : List Nat)
+    : List Nat
+    :=
   indices.filter (fun index => !session.context.any (·.id == index))
 
-def removeContext (session : Session) (input : String) (indices : List Nat) :
-    Except String Session :=
+def removeContext
+    (session : Session)
+    (input : String)
+    (indices : List Nat)
+    : Except String Session
+    :=
   let indices := indices.eraseDups
   if indices.isEmpty then
     .error "remove expects at least one context index"
@@ -198,15 +280,24 @@ def removeContext (session : Session) (input : String) (indices : List Nat) :
         let removed := String.intercalate ", " (indices.map contextIndexText)
         .ok (record session input s!"removed {removed}")
 
-private def singleStatement (source : String) : Except String _root_.TPTP.Statement := do
+private
+def singleStatement
+    (source : String)
+    : Except String _root_.TPTP.Statement
+    := do
   let document ← parseDocument source
   match document.items.toList with
   | [.statement statement] => pure statement
   | [] => .error "update expects one TPTP statement"
   | _ => .error "update expects exactly one TPTP statement"
 
-def updateContext (session : Session) (input : String) (index : Nat) (source : String) :
-    Except String Session := do
+def updateContext
+    (session : Session)
+    (input : String)
+    (index : Nat)
+    (source : String)
+    : Except String Session
+    := do
   let statement ← singleStatement source
   match session.context.find? (·.id == index) with
   | some item =>
@@ -220,7 +311,10 @@ def updateContext (session : Session) (input : String) (index : Nat) (source : S
           pure (record session input s!"updated {contextIndexText index}")
   | none => .error s!"unknown context index {contextIndexText index}"
 
-def problem (session : Session) : Option Problem :=
+def problem
+    (session : Session)
+    : Option Problem
+    :=
   if session.problemSource.isEmpty then none else some {
     name := "oatp-repl"
     source := session.problemSource
diff --git a/OATP/ReplView.lean b/OATP/ReplView.lean
index 9bdb735..d72e882 100644
--- a/OATP/ReplView.lean
+++ b/OATP/ReplView.lean
@@ -35,7 +35,9 @@ open scoped TermColor.Style
 
 def version : String := OATP.version
 
-def aurora : ColorScheme where
+def aurora
+    : ColorScheme
+    where
   background := .rgb 13 24 37
   foreground := .rgb 225 241 245
   selection := .rgb 39 70 83
@@ -49,7 +51,9 @@ def aurora : ColorScheme where
   purple := .rgb 178 146 255
   pink := .rgb 245 132 203
 
-def themes : List (String × ColorScheme) :=
+def themes
+    : List (String × ColorScheme)
+    :=
   [("aurora", aurora), ("terracotta", {
     background := .rgb 26 28 38
     foreground := .rgb 214 216 226
@@ -78,7 +82,10 @@ structure SemanticColors where
   functionColor : Color
   predicateColor : Color
 
-def semanticColors (scheme : ColorScheme) : SemanticColors where
+def semanticColors
+    (scheme : ColorScheme)
+    : SemanticColors
+    where
   format := scheme.cyan
   role := scheme.purple
   error := scheme.red
@@ -124,7 +131,9 @@ inductive AppContext
   | history
   | historyInput
 
-def AppContext.name : AppContext → String
+def AppContext.name
+    : AppContext →
+      String
   | .default => "default"
   | .run => "run"
   | .runInput => "run-input"
@@ -135,7 +144,9 @@ def AppContext.name : AppContext → String
   | .history => "history"
   | .historyInput => "history-input"
 
-def AppContext.keyContext : AppContext → KeyContext
+def AppContext.keyContext
+    : AppContext →
+      KeyContext
   | .default => KeyContext.ofString "default"
   | .run => KeyContext.ofString "run"
   | .runInput => KeyContext.ofString "run-input"
@@ -146,15 +157,23 @@ def AppContext.keyContext : AppContext → KeyContext
   | .history => KeyContext.ofString "history"
   | .historyInput => KeyContext.ofString "history-input"
 
-private def appBinding (keys : List Key) (action : AppKeyAction)
-    (context : Option AppContext) (description : String) : BindingSpec AppKeyAction :=
+private
+def appBinding
+    (keys : List Key)
+    (action : AppKeyAction)
+    (context : Option AppContext)
+    (description : String)
+    : BindingSpec AppKeyAction
+    :=
   { keys
     action
     context := context.map AppContext.keyContext
     label := String.intercalate "/" (keys.map Keymap.keyLabel)
     description }
 
-def appBindings : List (BindingSpec AppKeyAction) :=
+def appBindings
+    : List (BindingSpec AppKeyAction)
+    :=
   [ appBinding [.ctrl 'R', .ctrl 'r'] .toggleRun none "toggle the run drawer"
   , appBinding [.ctrl 'H', .ctrl 'h'] .toggleHistory none "toggle the history drawer"
   , appBinding [.ctrl 'S', .ctrl 's'] .toggleState none "toggle the state drawer"
@@ -180,12 +199,19 @@ def appBindings : List (BindingSpec AppKeyAction) :=
   , appBinding [.pageUp] .transcriptPageUp (some .default) "scroll transcript up"
   , appBinding [.pageDown] .transcriptPageDown (some .default) "scroll transcript down" ]
 
-def appKeyLabel (action : AppKeyAction) (context : AppContext) : String :=
+def appKeyLabel
+    (action : AppKeyAction)
+    (context : AppContext)
+    : String
+    :=
   (appBindings.find? (fun binding => binding.action == action &&
     (binding.context == none || binding.context == some (AppContext.keyContext context)))).map
       (·.label) |>.getD "?"
 
-def themeByName (name : String) : Option ColorScheme :=
+def themeByName
+    (name : String)
+    : Option ColorScheme
+    :=
   themes.find? (fun pair => pair.1 == name) |>.map Prod.snd
 
 def themeNames : String := String.intercalate ", " (themes.map Prod.fst)
@@ -221,7 +247,9 @@ inductive RunStatus where
 
 namespace RunStatus
 
-def label : RunStatus → String
+def label
+    : RunStatus →
+      String
   | .queued => "queued"
   | .running => "running"
   | .result status => s!"{status}"
@@ -253,10 +281,14 @@ inductive ContextTarget where
 
 namespace ContextTarget
 
-def all : List ContextTarget :=
+def all
+    : List ContextTarget
+    :=
   [.formulas, .symbols, .problem, .goal, .translation, .term]
 
-def name : ContextTarget → String
+def name
+    : ContextTarget →
+      String
   | .formulas => "formulas"
   | .symbols => "symbols"
   | .problem => "problem"
@@ -264,7 +296,9 @@ def name : ContextTarget → String
   | .translation => "translation"
   | .term => "term"
 
-def label : ContextTarget → String
+def label
+    : ContextTarget →
+      String
   | .formulas => "FORMULAS"
   | .symbols => "SYMBOLS"
   | .problem => "PROBLEM"
@@ -272,7 +306,9 @@ def label : ContextTarget → String
   | .translation => "LEAN → TPTP"
   | .term => "CHECKED TERM"
 
-def aliases : ContextTarget → List String
+def aliases
+    : ContextTarget →
+      List String
   | .formulas => ["form", "formula", "formulas"]
   | .symbols => ["symbol", "symbols"]
   | .problem => ["problem"]
@@ -280,7 +316,12 @@ def aliases : ContextTarget → List String
   | .translation => ["translation", "tptp"]
   | .term => ["term", "checked-term", "checked"]
 
-private def indexOf (value : String) : List ContextTarget → Nat → Option Nat
+private
+def indexOf
+    (value : String)
+    : List ContextTarget →
+      Nat →
+      Option Nat
   | [], _ => none
   | contextTarget :: rest, index =>
       if (aliases contextTarget).any (· == value) then some index
@@ -336,21 +377,31 @@ def fallbackSize : Size := { columns := 110, rows := 28 }
 
 def inputConfig : TextInputConfig := { width := 160, maxLength := 16_384 }
 
-def multilineConfig : MultilineConfig :=
+def multilineConfig
+    : MultilineConfig
+    :=
   { text := inputConfig, lineBreak := .ctrl 'n' }
 
 private def minFrameWidth : Nat := 34
 
 private def frameWidth (width : Nat) : Nat := max minFrameWidth width
 
-private def boxInnerWidth (outer : Nat) : Nat :=
+private
+def boxInnerWidth
+    (outer : Nat)
+    : Nat
+    :=
   Layout.boxInnerWidth { padding := 1 } outer
 
 private def panelWidth (width : Nat) : Nat := frameWidth width - 2
 
 private def stateDrawerMinWidth : Nat := 70
 
-private def stateDrawerWidths (width : Nat) : Option (Nat × Nat) :=
+private
+def stateDrawerWidths
+    (width : Nat)
+    : Option (Nat × Nat)
+    :=
   let total := frameWidth width
   if total < stateDrawerMinWidth then none
   else
@@ -358,36 +409,71 @@ private def stateDrawerWidths (width : Nat) : Option (Nat × Nat) :=
     let right := max 34 (available * 2 / 5)
     some (available - right, right)
 
-def drawerWidths (width : Nat) : Option (Nat × Nat) :=
+def drawerWidths
+    (width : Nat)
+    : Option (Nat × Nat)
+    :=
   stateDrawerWidths width
 
-private def joinLines : List Text → Text
+private
+def joinLines
+    : List Text →
+      Text
   | [] => Text.empty
   | line :: lines => lines.foldl (fun result next => result ++ Text.plain "\n" ++ next) line
 
-private def fitText (width : Nat) (value : String) : Text :=
+private
+def fitText
+    (width : Nat)
+    (value : String)
+    : Text
+    :=
   truncate width (Text.plain value)
 
-private def fillHeight (height : Nat) (text : Text) : Text :=
+private
+def fillHeight
+    (height : Nat)
+    (text : Text)
+    : Text
+    :=
   let height := max 1 height
   let lines := (splitLines text).take height
   joinLines (lines ++ List.replicate (height - lines.length) Text.empty)
 
-private def withBackground (scheme : ColorScheme) (text : Text) : Text :=
+private
+def withBackground
+    (scheme : ColorScheme)
+    (text : Text)
+    : Text
+    :=
   { segments := text.segments.map fun segment =>
       { segment with style := Style.bg scheme.background <+> segment.style } }
 
-private def dimText (text : Text) : Text :=
+private
+def dimText
+    (text : Text)
+    : Text
+    :=
   { segments := text.segments.map fun segment =>
       { segment with style := Style.dim <+> segment.style } }
 
-private def base64Alphabet : String :=
+private
+def base64Alphabet
+    : String
+    :=
   "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"
 
-private def base64Char (index : Nat) : Char :=
+private
+def base64Char
+    (index : Nat)
+    : Char
+    :=
   base64Alphabet.toList.getD index 'A'
 
-private def base64 : List UInt8 → String
+private
+def base64
+    : List UInt8 →
+      String
   | a :: b :: c :: rest =>
       let value := a.toNat * 65_536 + b.toNat * 256 + c.toNat
       String.ofList [base64Char (value / 262_144), base64Char ((value / 4_096) % 64),
@@ -401,11 +487,21 @@ private def base64 : List UInt8 → String
       String.ofList [base64Char (value / 4), base64Char ((value % 4) * 16), '=', '=']
   | [] => ""
 
-private def clipboardSequence (value : String) : String :=
+private
+def clipboardSequence
+    (value : String)
+    : String
+    :=
   "\u001b]52;c;" ++ base64 value.toUTF8.toList ++ "\u0007"
 
-private def opaqueScreen (scheme : ColorScheme) (size : Size) (content : Text)
-    (copyPending : Option String := none) : Text :=
+private
+def opaqueScreen
+    (scheme : ColorScheme)
+    (size : Size)
+    (content : Text)
+    (copyPending : Option String := none)
+    : Text
+    :=
   let width := max 1 size.columns
   let rows := max 1 size.rows
   let blank := Text.styled (String.ofList (List.replicate width ' '))
@@ -417,29 +513,52 @@ private def opaqueScreen (scheme : ColorScheme) (size : Size) (content : Text)
   | some value => screen ++ Text.plain (clipboardSequence value)
   | none => screen
 
-def formatElapsed (milliseconds : Nat) : String :=
+def formatElapsed
+    (milliseconds : Nat)
+    : String
+    :=
   if milliseconds == 0 then "<1 ms"
   else if milliseconds < 1_000 then s!"{milliseconds} ms"
   else s!"{milliseconds / 1_000}.{milliseconds % 1_000 / 100} s"
 
-private def diagnosticView (scheme : ColorScheme) (width : Nat) (sources : Sources)
-    (diagnostic : Diagnostic) : Text :=
+private
+def diagnosticView
+    (scheme : ColorScheme)
+    (width : Nat)
+    (sources : Sources)
+    (diagnostic : Diagnostic)
+    : Text
+    :=
   TermColor.Diagnostics.render sources diagnostic
     { width := max 1 (frameWidth width - 2), contextLines := 0, hyperlinks := false } scheme
 
-private def identifierChar (character : Char) : Bool :=
+private
+def identifierChar
+    (character : Char)
+    : Bool
+    :=
   character.isAlpha || character.isDigit || character == '_' || character == '$' ||
     character == '\''
 
-private def roleStyle (semantic : SemanticColors) : _root_.TPTP.Role → Option Style
+private
+def roleStyle
+    (semantic : SemanticColors)
+    : _root_.TPTP.Role →
+      Option Style
   | .axiom | .hypothesis | .definition | .assumption | .lemma | .theorem | .corollary
     | .conjecture | .negatedConjecture | .plain | .type | .interpretation | .logic
     | .unknown | .finiteDomain | .finiteFunctor | .finitePredicate =>
       some (Style.fg semantic.role)
   | .other _ => none
 
-private def symbolStyle (scheme : ColorScheme) (symbols : Array Symbol) (token : String)
-    (highlightSyntax : Bool := true) : Style :=
+private
+def symbolStyle
+    (scheme : ColorScheme)
+    (symbols : Array Symbol)
+    (token : String)
+    (highlightSyntax : Bool := true)
+    : Style
+    :=
   let lower := token.toLower
   let semantic := semanticColors scheme
   if token.startsWith "/" then Style.bold <+> Style.fg scheme.orange
@@ -463,14 +582,25 @@ private def symbolStyle (scheme : ColorScheme) (symbols : Array Symbol) (token :
                   | .predicate => Style.fg semantic.predicateColor
               | none => Style.fg scheme.foreground
 
-private def operatorStyle (scheme : ColorScheme) (token : String) : Style :=
+private
+def operatorStyle
+    (scheme : ColorScheme)
+    (token : String)
+    : Style
+    :=
   if token == "!" || token == "?" then Style.fg scheme.pink
   else if token == "(" || token == ")" || token == "[" || token == "]" || token == "," ||
       token == ":" || token == "." || token == ";" then Style.fg scheme.purple
   else Style.fg scheme.blue
 
-private def semanticText (scheme : ColorScheme) (symbols : Array Symbol) (value : String)
-    (highlightSyntax : Bool := true) : Text :=
+private
+def semanticText
+    (scheme : ColorScheme)
+    (symbols : Array Symbol)
+    (value : String)
+    (highlightSyntax : Bool := true)
+    : Text
+    :=
   let flush := fun (state : Text × String) =>
     if state.2.isEmpty then state
     else (state.1 ++ Text.styled state.2
@@ -492,11 +622,21 @@ private def semanticText (scheme : ColorScheme) (symbols : Array Symbol) (value
         (state.1 ++ Text.plain token, "")
   (flush (value.toList.foldl step (Text.empty, ""))).1
 
-private def semanticFormula (scheme : ColorScheme) (formula : FormulaView) : Text :=
+private
+def semanticFormula
+    (scheme : ColorScheme)
+    (formula : FormulaView)
+    : Text
+    :=
   semanticText scheme formula.symbols formula.formula
 
-private def formulaLine (scheme : ColorScheme) (selected : Option Nat)
-    (formula : FormulaView) : Text :=
+private
+def formulaLine
+    (scheme : ColorScheme)
+    (selected : Option Nat)
+    (formula : FormulaView)
+    : Text
+    :=
   let marker := if selected == some formula.id then "▸ " else "  "
   Text.styled s!"{marker}index #{formula.id} • cell {formula.cell} • {formula.role} "
       (Style.dim <+> Style.fg scheme.comment) ++
@@ -513,20 +653,38 @@ private def reportWidgetConfig (scheme : ColorScheme) : CollapsibleConfig := {
   overflowText := Text.styled "… more" (Style.dim <+> Style.fg scheme.comment)
   emptyText := Text.styled "(no report details)" (Style.dim <+> Style.fg scheme.comment) }
 
-private def reportSummary (scheme : ColorScheme) (report : Report) : Text :=
+private
+def reportSummary
+    (scheme : ColorScheme)
+    (report : Report)
+    : Text
+    :=
   let marker := match report.severity with
     | .error => Text.styled "issues" (Style.bold <+> Style.fg scheme.red)
     | .warning => Text.styled "warning" (Style.bold <+> Style.fg scheme.yellow)
     | _ => Text.styled "check" (Style.bold <+> Style.fg scheme.green)
   marker ++ Text.plain s!" • {report.title} • click to expand • Ctrl-R full output"
 
-private def reportBody (scheme : ColorScheme) (symbols : Array Symbol) (width : Nat)
-    (entry : TranscriptEntry) (report : Report) : Text :=
+private
+def reportBody
+    (scheme : ColorScheme)
+    (symbols : Array Symbol)
+    (width : Nat)
+    (entry : TranscriptEntry)
+    (report : Report)
+    : Text
+    :=
   renderReport report { width := max 1 (width - 6) } scheme ++ Text.plain "\n" ++
     semanticText scheme symbols entry.output false
 
-private def transcriptLine (scheme : ColorScheme) (symbols : Array Symbol) (width : Nat)
-    (entry : TranscriptEntry) : Text :=
+private
+def transcriptLine
+    (scheme : ColorScheme)
+    (symbols : Array Symbol)
+    (width : Nat)
+    (entry : TranscriptEntry)
+    : Text
+    :=
   let input := Text.styled s!"[{entry.cell}] " (Style.dim <+> Style.fg scheme.comment) ++
     Text.styled "› " (Style.bold <+> Style.fg scheme.orange) ++
     semanticText scheme symbols entry.input false
@@ -558,24 +716,43 @@ private def transcriptLine (scheme : ColorScheme) (symbols : Array Symbol) (widt
         (Style.dim <+> Style.fg scheme.comment)) |>.getD Text.empty
   input ++ Text.plain "\n" ++ output ++ timing
 
-private def spacedEntries : List Text → List Text
+private
+def spacedEntries
+    : List Text →
+      List Text
   | [] => []
   | [entry] => [entry]
   | entry :: rest => entry :: Text.empty :: spacedEntries rest
 
-private def transcriptLines (scheme : ColorScheme) (symbols : Array Symbol) (width : Nat)
-    (entries : List TranscriptEntry) : List Text :=
+private
+def transcriptLines
+    (scheme : ColorScheme)
+    (symbols : Array Symbol)
+    (width : Nat)
+    (entries : List TranscriptEntry)
+    : List Text
+    :=
   let views := entries.reverse.map (transcriptLine scheme symbols width)
   (spacedEntries views).flatMap splitLines
 
-private def reportWidget (scheme : ColorScheme) (symbols : Array Symbol) (width : Nat)
-    (entry : TranscriptEntry) : Option CollapsibleRender := do
+private
+def reportWidget
+    (scheme : ColorScheme)
+    (symbols : Array Symbol)
+    (width : Nat)
+    (entry : TranscriptEntry)
+    : Option CollapsibleRender
+    := do
   let report ← entry.report
   pure <| renderCollapsible (reportWidgetConfig scheme) (max 1 (width - 2))
     (reportSummary scheme report) (reportBody scheme symbols width entry report)
     { expanded := entry.reportExpanded }
 
-def reportAtTranscriptRow (app : App) (width row : Nat) : Option Nat :=
+def reportAtTranscriptRow
+    (app : App)
+    (width row : Nat)
+    : Option Nat
+    :=
   let rec find : List TranscriptEntry → Nat → Option Nat
     | [], _ => none
     | entry :: rest, offset =>
@@ -590,19 +767,33 @@ def reportAtTranscriptRow (app : App) (width row : Nat) : Option Nat :=
         | _, _ => find rest (offset + lineCount + 1)
   find app.entries.reverse 0
 
-def toggleReportCell (app : App) (cell : Nat) : App :=
+def toggleReportCell
+    (app : App)
+    (cell : Nat)
+    : App
+    :=
   { app with
     entries := app.entries.map fun entry =>
       if entry.cell == cell then { entry with reportExpanded := !entry.reportExpanded } else entry }
 
-private def visibleTranscriptLines (app : App) (width budget : Nat) : List Text :=
+private
+def visibleTranscriptLines
+    (app : App)
+    (width budget : Nat)
+    : List Text
+    :=
   let lines := transcriptLines app.theme app.session.symbols width app.entries
   let scroll := min app.transcriptScroll (lines.length - budget)
   let visibleEnd := lines.length - scroll
   let start := visibleEnd - min budget visibleEnd
   (lines.drop start).take (visibleEnd - start)
 
-private def transcript (app : App) (width budget bodyStart : Nat) : Text :=
+private
+def transcript
+    (app : App)
+    (width budget bodyStart : Nat)
+    : Text
+    :=
   let lines := visibleTranscriptLines app width budget
   if lines.isEmpty then
     Text.styled "Type a TPTP statement or /help." (Style.dim <+> Style.fg app.theme.comment)
@@ -620,25 +811,50 @@ private def transcript (app : App) (width budget bodyStart : Nat) : Text :=
           else line
     | _, _ => body
 
-private def selectionLines (app : App) (width budget : Nat) : List String :=
+private
+def selectionLines
+    (app : App)
+    (width budget : Nat)
+    : List String
+    :=
   (visibleTranscriptLines app width budget).map (·.plainText)
 
-def scrollTranscriptUp (app : App) : App :=
+def scrollTranscriptUp
+    (app : App)
+    : App
+    :=
   { app with transcriptScroll := app.transcriptScroll + 3 }
 
-def scrollTranscriptDown (app : App) : App :=
+def scrollTranscriptDown
+    (app : App)
+    : App
+    :=
   { app with transcriptScroll := app.transcriptScroll - min 3 app.transcriptScroll }
 
-def scrollTranscriptPageUp (app : App) : App :=
+def scrollTranscriptPageUp
+    (app : App)
+    : App
+    :=
   { app with transcriptScroll := app.transcriptScroll + 10 }
 
-def scrollTranscriptPageDown (app : App) : App :=
+def scrollTranscriptPageDown
+    (app : App)
+    : App
+    :=
   { app with transcriptScroll := app.transcriptScroll - min 10 app.transcriptScroll }
 
-def clearSelection (app : App) : App :=
+def clearSelection
+    (app : App)
+    : App
+    :=
   { app with selectionStart := none, selectionEnd := none }
 
-private def symbolLine (scheme : ColorScheme) (symbol : Symbol) : Text :=
+private
+def symbolLine
+    (scheme : ColorScheme)
+    (symbol : Symbol)
+    : Text
+    :=
   let kind := match symbol.kind with
     | .variable => "var"
     | .constant => "const"
@@ -649,7 +865,11 @@ private def symbolLine (scheme : ColorScheme) (symbol : Symbol) : Text :=
     Text.styled symbol.name (symbolStyle scheme #[symbol] symbol.name) ++
     Text.styled s!"/{symbol.arity}" (Style.dim <+> Style.fg scheme.comment)
 
-private def contextWidgetConfig (scheme : ColorScheme) : CollapsibleConfig where
+private
+def contextWidgetConfig
+    (scheme : ColorScheme)
+    : CollapsibleConfig
+    where
   collapsedMarker := Text.styled "▸ " (Style.fg scheme.comment)
   expandedMarker := Text.styled "▾ " (Style.fg scheme.orange)
   summaryStyle := Style.bold <+> Style.fg scheme.purple
@@ -660,7 +880,11 @@ private def contextWidgetConfig (scheme : ColorScheme) : CollapsibleConfig where
   overflowText := Text.styled "… more" (Style.dim <+> Style.fg scheme.comment)
   emptyText := Text.styled "(none)" (Style.dim <+> Style.fg scheme.comment)
 
-private def contextSections (app : App) : List (Nat × Text × Text) :=
+private
+def contextSections
+    (app : App)
+    : List (Nat × Text × Text)
+    :=
   let formulas := app.session.formulas.toList.reverse.take 8
   let symbols := app.session.symbols.toList.take 12
   let problem := if app.session.context.isEmpty then
@@ -703,14 +927,29 @@ private def contextSections (app : App) : List (Nat × Text × Text) :=
 
 #guard (contextSections ({} : App)).isEmpty
 
-private def contextExpandedAt (app : App) (index : Nat) : Bool :=
+private
+def contextExpandedAt
+    (app : App)
+    (index : Nat)
+    : Bool
+    :=
   app.contextExpanded.getD index true
 
-private def contextState (app : App) (index : Nat) : CollapsibleState :=
+private
+def contextState
+    (app : App)
+    (index : Nat)
+    : CollapsibleState
+    :=
   { expanded := contextExpandedAt app index
     focused := app.contextFocus == index }
 
-private def contextRenders (app : App) (width : Nat) : List (Nat × CollapsibleRender) :=
+private
+def contextRenders
+    (app : App)
+    (width : Nat)
+    : List (Nat × CollapsibleRender)
+    :=
   let innerWidth := max 1 (boxInnerWidth width)
   let rec go : List (Nat × Text × Text) → List (Nat × CollapsibleRender)
     | [] => []
@@ -719,10 +958,19 @@ private def contextRenders (app : App) (width : Nat) : List (Nat × CollapsibleR
           (contextState app index)) :: go sections
   go (contextSections app)
 
-private def contextTexts (app : App) (width : Nat) : List Text :=
+private
+def contextTexts
+    (app : App)
+    (width : Nat)
+    : List Text
+    :=
   (contextRenders app width).map (fun (_, widget) => widget.text)
 
-def contextHitAtRow (app : App) (width row : Nat) : Option (Nat × Bool) :=
+def contextHitAtRow
+    (app : App)
+    (width row : Nat)
+    : Option (Nat × Bool)
+    :=
   if row < 2 then none
   else
     let relativeRow := row - 2
@@ -734,7 +982,11 @@ def contextHitAtRow (app : App) (width row : Nat) : Option (Nat × Bool) :=
           else find renders (offset + widget.lineCount)
     find (contextRenders app width) 0
 
-def contextFormulaAtRow (app : App) (width row : Nat) : Option Nat :=
+def contextFormulaAtRow
+    (app : App)
+    (width row : Nat)
+    : Option Nat
+    :=
   match contextHitAtRow app width row with
   | some (0, false) =>
       let relativeRow := row - 2
@@ -746,16 +998,35 @@ def contextFormulaAtRow (app : App) (width row : Nat) : Option Nat :=
       | [] => none
   | _ => none
 
-private def updateContextExpanded (app : App) (index : Nat) (expanded : Bool) : App :=
+private
+def updateContextExpanded
+    (app : App)
+    (index : Nat)
+    (expanded : Bool)
+    : App
+    :=
   { app with contextExpanded := app.contextExpanded.set! index expanded }
 
-def focusContext (app : App) (index : Nat) : App :=
+def focusContext
+    (app : App)
+    (index : Nat)
+    : App
+    :=
   { app with contextFocus := min (contextSectionCount - 1) index }
 
-private def visibleContextIndices (app : App) : Array Nat :=
+private
+def visibleContextIndices
+    (app : App)
+    : Array Nat
+    :=
   (contextSections app).map (fun (index, _, _) => index) |>.toArray
 
-private def moveContext (app : App) (forward : Bool) : App :=
+private
+def moveContext
+    (app : App)
+    (forward : Bool)
+    : App
+    :=
   let indices := visibleContextIndices app
   if indices.isEmpty then
     app
@@ -768,21 +1039,41 @@ private def moveContext (app : App) (forward : Bool) : App :=
         let offset := if forward then 1 else indices.size - 1
         focusContext app (indices[(current + offset) % indices.size]?.getD app.contextFocus)
 
-def focusNextContext (app : App) : App :=
+def focusNextContext
+    (app : App)
+    : App
+    :=
   moveContext app true
 
-def focusPreviousContext (app : App) : App :=
+def focusPreviousContext
+    (app : App)
+    : App
+    :=
   moveContext app false
 
-private def formulaIds (app : App) : List Nat :=
+private
+def formulaIds
+    (app : App)
+    : List Nat
+    :=
   app.session.formulas.toList.reverse.map (·.id)
 
-private def indexOfFormula : Nat → Nat → List Nat → Option Nat
+private
+def indexOfFormula
+    : Nat →
+      Nat →
+      List Nat →
+      Option Nat
   | _, _, [] => none
   | wanted, index, id :: ids =>
       if wanted == id then some index else indexOfFormula wanted (index + 1) ids
 
-private def nextFormulaId (app : App) (forward : Bool) : Option Nat :=
+private
+def nextFormulaId
+    (app : App)
+    (forward : Bool)
+    : Option Nat
+    :=
   let ids := formulaIds app |>.take 8
   match ids with
   | [] => none
@@ -793,66 +1084,114 @@ private def nextFormulaId (app : App) (forward : Bool) : Option Nat :=
           let index := (indexOfFormula current 0 ids).getD 0
           if forward then ids[index + 1]? else if index == 0 then none else ids[index - 1]?
 
-def focusContextItem (app : App) (id : Nat) : App :=
+def focusContextItem
+    (app : App)
+    (id : Nat)
+    : App
+    :=
   if app.session.formulas.any (·.id == id) then
     { app with contextFocus := 0, contextItemFocus := some id }
   else app
 
-def focusNextContextItem (app : App) : App :=
+def focusNextContextItem
+    (app : App)
+    : App
+    :=
   match nextFormulaId app true with
   | some id => focusContextItem app id
   | none => { app with contextItemFocus := none }
 
-def focusPreviousContextItem (app : App) : App :=
+def focusPreviousContextItem
+    (app : App)
+    : App
+    :=
   match nextFormulaId app false with
   | some id => focusContextItem app id
   | none => { app with contextItemFocus := none }
 
-def focusNextContextEntry (app : App) : App :=
+def focusNextContextEntry
+    (app : App)
+    : App
+    :=
   if app.contextFocus == 0 && app.session.formulas.isEmpty == false then
     match nextFormulaId app true with
     | some id => focusContextItem app id
     | none => moveContext app true
   else focusNextContext app
 
-def focusPreviousContextEntry (app : App) : App :=
+def focusPreviousContextEntry
+    (app : App)
+    : App
+    :=
   if app.contextFocus == 0 && app.session.formulas.isEmpty == false then
     match nextFormulaId app false with
     | some id => focusContextItem app id
     | none => moveContext app false
   else focusPreviousContext app
 
-def toggleFocusedContext (app : App) : App :=
+def toggleFocusedContext
+    (app : App)
+    : App
+    :=
   updateContextExpanded app app.contextFocus (!contextExpandedAt app app.contextFocus)
 
-def expandFocusedContext (app : App) : App :=
+def expandFocusedContext
+    (app : App)
+    : App
+    :=
   updateContextExpanded app app.contextFocus true
 
-def collapseFocusedContext (app : App) : App :=
+def collapseFocusedContext
+    (app : App)
+    : App
+    :=
   updateContextExpanded app app.contextFocus false
 
-def focusProver (app : App) (index : Nat) : App :=
+def focusProver
+    (app : App)
+    (index : Nat)
+    : App
+    :=
   let focus := if app.proverChoices.isEmpty then 0 else min (app.proverChoices.size - 1) index
   { app with proverFocus := focus }
 
-def focusNextProver (app : App) : App :=
+def focusNextProver
+    (app : App)
+    : App
+    :=
   focusProver app ((app.proverFocus + 1) % max 1 app.proverChoices.size)
 
-def focusPreviousProver (app : App) : App :=
+def focusPreviousProver
+    (app : App)
+    : App
+    :=
   focusProver app (if app.proverFocus == 0 then max 1 app.proverChoices.size - 1
     else app.proverFocus - 1)
 
-def focusRun (app : App) (index : Nat) : App :=
+def focusRun
+    (app : App)
+    (index : Nat)
+    : App
+    :=
   let focus := if app.runRows.isEmpty then 0 else min (app.runRows.size - 1) index
   { app with runFocus := focus }
 
-def focusNextRun (app : App) : App :=
+def focusNextRun
+    (app : App)
+    : App
+    :=
   focusRun app ((app.runFocus + 1) % max 1 app.runRows.size)
 
-def focusPreviousRun (app : App) : App :=
+def focusPreviousRun
+    (app : App)
+    : App
+    :=
   focusRun app (if app.runFocus == 0 then max 1 app.runRows.size - 1 else app.runFocus - 1)
 
-def toggleFocusedProver (app : App) : App :=
+def toggleFocusedProver
+    (app : App)
+    : App
+    :=
   if app.proverChoices.isEmpty then app else
     let reference := app.proverChoices[app.proverFocus]!
     let enabled := app.enabledProvers.any (· == reference)
@@ -863,13 +1202,23 @@ def toggleFocusedProver (app : App) : App :=
     { updated with statusNotice := some s!"{ProverReference.display reference} {
       if enabled then "disabled" else "enabled"}" }
 
-def contextTargetNames : List String :=
+def contextTargetNames
+    : List String
+    :=
   ContextTarget.all.map ContextTarget.name
 
-def contextTargetOfString (value : String) : Option Nat :=
+def contextTargetOfString
+    (value : String)
+    : Option Nat
+    :=
   ContextTarget.indexOfString value
 
-private def prepareContextCommand (app : App) (command : String) : App :=
+private
+def prepareContextCommand
+    (app : App)
+    (command : String)
+    : App
+    :=
   match app.contextItemFocus with
   | none => { app with statusNotice := some "select a formula in the FORMULAS box first" }
   | some id =>
@@ -890,7 +1239,11 @@ def removeContextItem (app : App) : App := prepareContextCommand app "remove"
 
 def editContextItem (app : App) : App := prepareContextCommand app "update"
 
-def openContextTarget (app : App) (target : String) : Option App :=
+def openContextTarget
+    (app : App)
+    (target : String)
+    : Option App
+    :=
   if target.toLower == "all" then
     let app := { app with stateOpen := true }
     some { app with contextExpanded := Array.replicate contextSectionCount true }
@@ -901,7 +1254,10 @@ def openContextTarget (app : App) (target : String) : Option App :=
         some (if index == 0 then focusNextContextItem app else app)
     | none => none
 
-def toggleStatePanel (app : App) : App :=
+def toggleStatePanel
+    (app : App)
+    : App
+    :=
   if app.stateOpen && app.panelFocus == .drawer then
     { app with stateOpen := false, panelFocus := .main }
   else
@@ -912,7 +1268,10 @@ def toggleStatePanel (app : App) : App :=
       runOpen := false
       panelFocus := .drawer }
 
-def toggleHistoryPanel (app : App) : App :=
+def toggleHistoryPanel
+    (app : App)
+    : App
+    :=
   if app.historyOpen && app.panelFocus == .drawer then
     { app with historyOpen := false, panelFocus := .main }
   else
@@ -923,7 +1282,10 @@ def toggleHistoryPanel (app : App) : App :=
       runOpen := false
       panelFocus := .drawer }
 
-def toggleRunPanel (app : App) : App :=
+def toggleRunPanel
+    (app : App)
+    : App
+    :=
   if app.runRows.isEmpty then
     { app with statusNotice := some "no prover run to inspect" }
   else if app.runOpen && app.panelFocus == .drawer then
@@ -936,7 +1298,12 @@ def toggleRunPanel (app : App) : App :=
       proversOpen := false
       panelFocus := .drawer }
 
-private def contextPanel (app : App) (width height : Nat) : Text :=
+private
+def contextPanel
+    (app : App)
+    (width height : Nat)
+    : Text
+    :=
   let body := joinLines (contextTexts app width)
   let innerWidth := boxInnerWidth width
   let body := padRight innerWidth (fillHeight (max 1 (height - 2)) body)
@@ -947,7 +1314,11 @@ private def contextPanel (app : App) (width height : Nat) : Text :=
            , borderStyle := Style.fg (if active then app.theme.selection else app.theme.comment)
            , maxWidth := some width }
 
-private def historyWidgetConfig (scheme : ColorScheme) : CollapsibleConfig where
+private
+def historyWidgetConfig
+    (scheme : ColorScheme)
+    : CollapsibleConfig
+    where
   collapsedMarker := Text.styled "▸ " (Style.fg scheme.comment)
   expandedMarker := Text.styled "▾ " (Style.fg scheme.orange)
   summaryStyle := Style.bold <+> Style.fg scheme.purple
@@ -957,8 +1328,13 @@ private def historyWidgetConfig (scheme : ColorScheme) : CollapsibleConfig where
   overflowText := Text.styled "… more" (Style.dim <+> Style.fg scheme.comment)
   emptyText := Text.styled "(empty help)" (Style.dim <+> Style.fg scheme.comment)
 
-private def historyWidget (app : App) (width : Nat) (entry : OATP.Repl.HistoryEntry) :
-    Option CollapsibleRender :=
+private
+def historyWidget
+    (app : App)
+    (width : Nat)
+    (entry : OATP.Repl.HistoryEntry)
+    : Option CollapsibleRender
+    :=
   if entry.input.startsWith "/help" then
     let expanded := app.historyExpanded.any (· == entry.cell)
     let lines := entry.result.splitOn "\n" |>.length
@@ -968,7 +1344,13 @@ private def historyWidget (app : App) (width : Nat) (entry : OATP.Repl.HistoryEn
       (max 1 (boxInnerWidth width - 2)) summary (Text.plain entry.result) { expanded }
   else none
 
-private def historyLine (app : App) (width : Nat) (entry : OATP.Repl.HistoryEntry) : Text :=
+private
+def historyLine
+    (app : App)
+    (width : Nat)
+    (entry : OATP.Repl.HistoryEntry)
+    : Text
+    :=
   let input := Text.styled s!"[{entry.cell}] " (Style.dim <+> Style.fg app.theme.comment) ++
     semanticText app.theme app.session.symbols entry.input false
   match historyWidget app width entry with
@@ -978,7 +1360,12 @@ private def historyLine (app : App) (width : Nat) (entry : OATP.Repl.HistoryEntr
       semanticText app.theme app.session.symbols
         (fitText (max 1 (width - 6)) entry.result).plainText false
 
-private def historyPanel (app : App) (width height : Nat) : Text :=
+private
+def historyPanel
+    (app : App)
+    (width height : Nat)
+    : Text
+    :=
   let rows := app.session.history.toList.reverse.take 18
   let body := if rows.isEmpty then
       Text.styled "No commands yet." (Style.dim <+> Style.fg app.theme.comment)
@@ -989,7 +1376,11 @@ private def historyPanel (app : App) (width height : Nat) : Text :=
       (Style.bold <+> Style.fg app.theme.cyan))
            , borderStyle := Style.fg app.theme.selection, maxWidth := some width }
 
-def historyCellAtRow (app : App) (width row : Nat) : Option Nat :=
+def historyCellAtRow
+    (app : App)
+    (width row : Nat)
+    : Option Nat
+    :=
   let rows := app.session.history.toList.reverse.take 18
   let rec find : List OATP.Repl.HistoryEntry → Nat → Option Nat
     | [], _ => none
@@ -1002,17 +1393,30 @@ def historyCellAtRow (app : App) (width row : Nat) : Option Nat :=
         if hit then some entry.cell else find rest (offset + line.height + 1)
   find rows 0
 
-def toggleHistoryCell (app : App) (cell : Nat) : App :=
+def toggleHistoryCell
+    (app : App)
+    (cell : Nat)
+    : App
+    :=
   let expanded := if app.historyExpanded.any (· == cell) then
       app.historyExpanded.filter (· != cell)
     else app.historyExpanded.push cell
   { app with historyExpanded := expanded }
 
-def proverVisibleStart (app : App) (height : Nat) : Nat :=
+def proverVisibleStart
+    (app : App)
+    (height : Nat)
+    : Nat
+    :=
   let visible := max 1 (height - 2)
   if app.proverFocus >= visible then app.proverFocus - visible + 1 else 0
 
-private def proverPanel (app : App) (width height : Nat) : Text :=
+private
+def proverPanel
+    (app : App)
+    (width height : Nat)
+    : Text
+    :=
   let visible := max 1 (height - 2)
   let start := proverVisibleStart app height
   let rows := if app.proverChoices.isEmpty then
@@ -1035,13 +1439,21 @@ private def proverPanel (app : App) (width height : Nat) : Text :=
            , borderStyle := Style.fg (if active then app.theme.selection else app.theme.comment)
            , maxWidth := some width }
 
-private def runStatusStyle (scheme : ColorScheme) : RunStatus → Style
+private
+def runStatusStyle
+    (scheme : ColorScheme)
+    : RunStatus →
+      Style
   | .result .theorem | .result .unsatisfiable => Style.bold <+> Style.fg scheme.green
   | .running | .queued => Style.fg scheme.yellow
   | .result .error | .failed => Style.bold <+> Style.fg scheme.red
   | _ => Style.fg scheme.comment
 
-private def runDetail (row : RunRow) : String :=
+private
+def runDetail
+    (row : RunRow)
+    : String
+    :=
   if !row.detail.isEmpty then row.detail else match row.status with
     | .queued => "queued; waiting for the previous prover"
     | .running => "waiting for the prover result"
@@ -1049,7 +1461,12 @@ private def runDetail (row : RunRow) : String :=
     | .failed => "the prover failed without additional output"
     | .cancelled => "run cancelled"
 
-private def runPanel (app : App) (width height : Nat) : Text :=
+private
+def runPanel
+    (app : App)
+    (width height : Nat)
+    : Text
+    :=
   let innerWidth := boxInnerWidth width
   let rows := if app.runRows.isEmpty then
       [Text.styled "No active prover run." (Style.dim <+> Style.fg app.theme.comment)]
@@ -1076,7 +1493,11 @@ private def runPanel (app : App) (width height : Nat) : Text :=
            , borderStyle := Style.fg (if active then app.theme.selection else app.theme.comment)
            , maxWidth := some width }
 
-private def mascot (scheme : ColorScheme) : Text :=
+private
+def mascot
+    (scheme : ColorScheme)
+    : Text
+    :=
   let arrow := Text.styled "──▶" (Style.fg scheme.cyan)
   joinLines [ Text.styled "TPTP" (Style.fg scheme.yellow) ++ Text.plain " " ++ arrow ++
                 Text.plain " " ++ Text.styled "OATP" (Style.bold <+> Style.fg scheme.green) ++
@@ -1085,7 +1506,12 @@ private def mascot (scheme : ColorScheme) : Text :=
             , Text.plain "          " ++ Text.styled "▼" (Style.fg scheme.cyan)
             , Text.plain "         " ++ Text.styled "LEAN ✓" (Style.fg scheme.blue) ]
 
-private def banner (scheme : ColorScheme) (width : Nat) : Text :=
+private
+def banner
+    (scheme : ColorScheme)
+    (width : Nat)
+    : Text
+    :=
   let outer := frameWidth width
   let inner := boxInnerWidth outer
   let leftContent :=
@@ -1133,7 +1559,12 @@ private def banner (scheme : ColorScheme) (width : Nat) : Text :=
       , titleAlignment := .left, borderStyle := Style.fg scheme.orange
       , maxWidth := some outer }
 
-private def compactHeader (scheme : ColorScheme) (width : Nat) : Text :=
+private
+def compactHeader
+    (scheme : ColorScheme)
+    (width : Nat)
+    : Text
+    :=
   let outer := frameWidth width
   let title := s!" oatp repl v{version} "
   let used := title.length + 2
@@ -1142,14 +1573,24 @@ private def compactHeader (scheme : ColorScheme) (width : Nat) : Text :=
     Text.styled (String.ofList (List.replicate (if outer > used then outer - used else 0) '─'))
       (Style.fg scheme.selection)
 
-def reportAtScreenRow (app : App) (size : Size) (row : Nat) : Option Nat :=
+def reportAtScreenRow
+    (app : App)
+    (size : Size)
+    (row : Nat)
+    : Option Nat
+    :=
   let width := frameWidth size.columns
   let head := if app.entries.isEmpty then banner app.theme width else compactHeader app.theme width
   let bodyStart := head.height + 1
   if row < bodyStart then none else reportAtTranscriptRow app width (row - bodyStart)
 
-def prompt (scheme : ColorScheme) (width : Nat) (state : Repl.State)
-    (focused : Bool := true) : Text :=
+def prompt
+    (scheme : ColorScheme)
+    (width : Nat)
+    (state : Repl.State)
+    (focused : Bool := true)
+    : Text
+    :=
   let outer := frameWidth width
   let input := box (Text.styled "› " (Style.bold <+> Style.fg scheme.orange) ++
       TermColor.Repl.renderMultilineTextInputBody
@@ -1165,7 +1606,12 @@ def prompt (scheme : ColorScheme) (width : Nat) (state : Repl.State)
         textStyle := Style.fg scheme.foreground
         kindStyle := Style.dim <+> Style.fg scheme.comment } menu
 
-private def footer (app : App) (width : Nat) : Text :=
+private
+def footer
+    (app : App)
+    (width : Nat)
+    : Text
+    :=
   let outer := frameWidth width
   let state := if app.busy then "[BUSY]" else "[READY]"
   let closeRun := appKeyLabel .closeRun .runInput
@@ -1209,7 +1655,11 @@ private def footer (app : App) (width : Nat) : Text :=
     , truncate rightWidth
         (Text.styled hint (Style.dim <+> Style.fg app.theme.comment)) ] [.left, .left]
 
-def selectedText (app : App) (size : Size) : String :=
+def selectedText
+    (app : App)
+    (size : Size)
+    : String
+    :=
   let width := frameWidth size.columns
   let head := if app.entries.isEmpty then banner app.theme width else compactHeader app.theme width
   let foot := prompt app.theme width app.repl (app.panelFocus == .main) ++
@@ -1227,7 +1677,12 @@ def selectedText (app : App) (size : Size) : String :=
       String.intercalate "\n" (lines.drop low |>.take (high - low + 1))
   | _, _ => ""
 
-private def calcContent (app : App) (size : Size) : Text :=
+private
+def calcContent
+    (app : App)
+    (size : Size)
+    : Text
+    :=
   let width := frameWidth size.columns
   let head := if app.entries.isEmpty then banner app.theme width else compactHeader app.theme width
   let foot := prompt app.theme width app.repl (app.panelFocus == .main) ++
@@ -1237,7 +1692,11 @@ private def calcContent (app : App) (size : Size) : Text :=
   let body := transcript app width budget (head.height + 1)
   head ++ Text.plain "\n" ++ fillHeight budget body ++ Text.plain "\n" ++ foot
 
-def screen (app : App) (size : Size) : Text :=
+def screen
+    (app : App)
+    (size : Size)
+    : Text
+    :=
   let width := frameWidth size.columns
   let size := { size with columns := width }
   let drawerOpen := app.runOpen || app.proversOpen ||
diff --git a/OATP/Runtime.lean b/OATP/Runtime.lean
index 89219b0..21d944c 100644
--- a/OATP/Runtime.lean
+++ b/OATP/Runtime.lean
@@ -24,7 +24,10 @@ inductive CatalogueCache where
   | refresh
   | noCache
 
-def readProblem (path : String) : IO Problem := do
+def readProblem
+    (path : String)
+    : IO Problem
+    := do
   pure { name := path, source := ← IO.FS.readFile path }
 
 def defaultLocalProverCandidates : Array String := #["eprover", "vampire", "metis"]
@@ -35,14 +38,18 @@ def doctorTimeoutSeconds : Nat := 5
 
 def doctorMaxOutputBytes : Nat := 1024 * 1024
 
-def localProverCandidates : IO (Array String) := do
+def localProverCandidates
+    : IO (Array String)
+    := do
   match ← IO.getEnv "OATP_LOCAL_PROVERS" with
   | some value =>
       pure <| value.splitOn "," |>.map (·.trimAscii.toString) |>.filter (!·.isEmpty) |>.toArray
   | none => pure defaultLocalProverCandidates
 
-def catalogueLocation (cacheNamespace endpoint : String) :
-    IO (Option (System.FilePath × System.FilePath)) := do
+def catalogueLocation
+    (cacheNamespace endpoint : String)
+    : IO (Option (System.FilePath × System.FilePath))
+    := do
   let root ← match ← IO.getEnv "XDG_CACHE_HOME" with
     | some path => pure (some (⟨path⟩ : System.FilePath))
     | none => match ← IO.getEnv "HOME" with
@@ -56,7 +63,9 @@ def catalogueLocation (cacheNamespace endpoint : String) :
     let directory := System.FilePath.join root cacheName
     (directory, System.FilePath.join directory s!"systems-{hash normalizedEndpoint}.html")
 
-def httpErrorMessage : OATP.Http.Error → String
+def httpErrorMessage
+    : OATP.Http.Error →
+      String
   | .io message => s!"HTTP IO failed: {message}"
   | .invalidRequest message => s!"invalid HTTP request: {message}"
   | .transport message => s!"HTTP transport failed: {message}"
@@ -66,9 +75,12 @@ def httpErrorMessage : OATP.Http.Error → String
   | .bodyTooLarge actual limit =>
       s!"HTTP response exceeded {limit} bytes ({actual} captured)"
 
-def fetchCatalogue (endpoint : String)
+def fetchCatalogue
+    (endpoint : String)
     (location : Option (System.FilePath × System.FilePath))
-    (writeCache : Bool) : IO (Except String (Array SystemOnTPTP.Catalogue.SystemInfo)) := do
+    (writeCache : Bool)
+    : IO (Except String (Array SystemOnTPTP.Catalogue.SystemInfo))
+    := do
   match ← SystemOnTPTP.fetchCatalogue endpoint with
   | .error error => pure (.error (httpErrorMessage error))
   | .ok response =>
@@ -87,8 +99,11 @@ def fetchCatalogue (endpoint : String)
               catch _ => pure ()
           pure (.ok systems)
 
-def loadCatalogue (cacheNamespace endpoint : String) (mode : CatalogueCache) :
-    IO (Except String (Array SystemOnTPTP.Catalogue.SystemInfo)) := do
+def loadCatalogue
+    (cacheNamespace endpoint : String)
+    (mode : CatalogueCache)
+    : IO (Except String (Array SystemOnTPTP.Catalogue.SystemInfo))
+    := do
   let location ← catalogueLocation cacheNamespace endpoint
   match mode with
   | .normal =>
@@ -104,15 +119,21 @@ def loadCatalogue (cacheNamespace endpoint : String) (mode : CatalogueCache) :
   | .refresh => fetchCatalogue endpoint location true
   | .noCache => fetchCatalogue endpoint none false
 
-def installedProvers : IO (Array String) := do
+def installedProvers
+    : IO (Array String)
+    := do
   let mut found := #[]
   for executable in ← localProverCandidates do
     if (← Http.commandVersion executable).isSome then
       found := found.push executable
   pure found
 
-def resolveOnline (toolName : String) (systems : Array SystemOnTPTP.Catalogue.SystemInfo)
-    (references : List String) : Except String (Array SystemOnTPTP.Catalogue.SystemInfo) := do
+def resolveOnline
+    (toolName : String)
+    (systems : Array SystemOnTPTP.Catalogue.SystemInfo)
+    (references : List String)
+    : Except String (Array SystemOnTPTP.Catalogue.SystemInfo)
+    := do
   let resolved ← references.mapM fun reference =>
     match SystemOnTPTP.Catalogue.resolve systems reference with
     | some system => pure system
diff --git a/OATP/SystemOnTPTP.lean b/OATP/SystemOnTPTP.lean
index 2466222..6ed8571 100644
--- a/OATP/SystemOnTPTP.lean
+++ b/OATP/SystemOnTPTP.lean
@@ -40,7 +40,10 @@ def isOnlineReference (reference : String) : Bool := reference.startsWith online
 
 def onlineReference (systemId : String) : String := onlineReferencePrefix ++ systemId
 
-def onlineSystemId (reference : String) : String :=
+def onlineSystemId
+    (reference : String)
+    : String
+    :=
   if isOnlineReference reference then
     (reference.drop onlineReferencePrefix.length).toString
   else reference
@@ -60,19 +63,35 @@ private inductive HtmlPart where
 
 open Grip GParser
 
-private def htmlTag : GParser conditional HtmlPart :=
+private
+def htmlTag
+    : GParser conditional HtmlPart
+    :=
   HtmlPart.tag <$> GParser.capture (GParser.ch '<' *> GParser.takeWhile (· != 62) <* GParser.ch '>')
 
-private def htmlText : GParser conditional HtmlPart :=
+private
+def htmlText
+    : GParser conditional HtmlPart
+    :=
   HtmlPart.text <$> GParser.capture (GParser.takeWhile1 (· != 60))
 
-private def htmlPart : GParser conditional HtmlPart :=
+private
+def htmlPart
+    : GParser conditional HtmlPart
+    :=
   GParser.chooseG htmlTag [htmlText]
 
-private def htmlDocument : Grip.Parser (List HtmlPart) :=
+private
+def htmlDocument
+    : Grip.Parser (List HtmlPart)
+    :=
   GParser.seqL (GParser.many htmlPart) GParser.eof
 
-private def parseHtml (source : String) : Except Grip.ParseError (List HtmlPart) :=
+private
+def parseHtml
+    (source : String)
+    : Except Grip.ParseError (List HtmlPart)
+    :=
   htmlDocument.parse source.toUTF8
 
 namespace Catalogue
@@ -83,29 +102,49 @@ structure SystemInfo where
   timeLimit : Nat := defaultSystemTimeLimit
   deriving BEq, DecidableEq, Repr
 
-private def quotedAfter (marker line : String) : Option String :=
+private
+def quotedAfter
+    (marker line : String)
+    : Option String
+    :=
   match line.splitOn marker with
   | _ :: value :: _ => some (value.splitOn "\"" |>.headD "")
   | _ => none
 
-private def systemId (line : String) : Option String :=
+private
+def systemId
+    (line : String)
+    : Option String
+    :=
   (quotedAfter "NAME=\"System___" line).orElse fun _ =>
     quotedAfter "name=\"System___" line
 
-private def fieldValue (field id current line : String) : String :=
+private
+def fieldValue
+    (field id current line : String)
+    : String
+    :=
   let lower := quotedAfter s!"name=\"{field}___{id}\"" line
   let upper := quotedAfter s!"NAME=\"{field}___{id}\"" line
   if lower.isSome || upper.isSome then
     (quotedAfter "value=\"" line).getD current
   else current
 
-private def updateInfo (line : String) (system : SystemInfo) : SystemInfo :=
+private
+def updateInfo
+    (line : String)
+    (system : SystemInfo)
+    : SystemInfo
+    :=
   let command := fieldValue "Command" system.id system.command line
   let timeLimit := (fieldValue "TimeLimit" system.id (toString system.timeLimit) line).toNat?.getD
     system.timeLimit
   { system with command, timeLimit }
 
-def parse (html : String) : Array SystemInfo :=
+def parse
+    (html : String)
+    : Array SystemInfo
+    :=
   match parseHtml html with
   | .error _ => #[]
   | .ok parts => parts.foldl (init := #[]) fun systems part =>
@@ -121,22 +160,38 @@ def parse (html : String) : Array SystemInfo :=
 
 def baseName (id : String) : String := id.splitOn "---" |>.headD id
 
-def matchesReference (reference : String) (system : SystemInfo) : Bool :=
+def matchesReference
+    (reference : String)
+    (system : SystemInfo)
+    : Bool
+    :=
   let reference := onlineSystemId reference
   let wanted := reference.toLower
   let id := system.id.toLower
   id == wanted || (baseName system.id).toLower == wanted ||
     id.startsWith (wanted ++ "---")
 
-def resolve (systems : Array SystemInfo) (reference : String) : Option SystemInfo :=
+def resolve
+    (systems : Array SystemInfo)
+    (reference : String)
+    : Option SystemInfo
+    :=
   systems.toList.find? (matchesReference reference)
 
 end Catalogue
 
-def labels (config : Config) : Array String :=
+def labels
+    (config : Config)
+    : Array String
+    :=
   if config.systemLabels.isEmpty then #[config.systemLabel] else config.systemLabels
 
-private def command (config : Config) (label : String) : String :=
+private
+def command
+    (config : Config)
+    (label : String)
+    : String
+    :=
   config.systemCommands.toList.find? (·.1 == label) |>.map (·.2) |>.getD "default"
 
 inductive ResponseError where
@@ -146,13 +201,19 @@ inductive ResponseError where
   | malformedBody (message : String)
   deriving Repr
 
-def ResponseError.message : ResponseError → String
+def ResponseError.message
+    : ResponseError →
+      String
   | .httpStatus status => s!"SystemOnTPTP returned HTTP {status}"
   | .missingStatus => "SystemOnTPTP response did not contain an SZS status"
   | .unsupportedStatus status => s!"SystemOnTPTP returned unsupported SZS status `{status}`"
   | .malformedBody message => s!"SystemOnTPTP response was not valid HTML: {message}"
 
-def fields (config : Config) (problem : Problem) : Array Field :=
+def fields
+    (config : Config)
+    (problem : Problem)
+    : Array Field
+    :=
   let base : Array Field := #[
     { name := "ProblemSource", value := "FORMULAE" },
     { name := "FORMULAEProblem", value := problem.source },
@@ -169,7 +230,11 @@ def fields (config : Config) (problem : Problem) : Array Field :=
     { name := s!"Transform___{label}", value := "none" }
   ]) base
 
-def request (config : Config) (problem : Problem) : Http.Request where
+def request
+    (config : Config)
+    (problem : Problem)
+    : Http.Request
+    where
   method := .post
   url := config.endpoint
   body := encodeUrlEncoded (fields config problem)
@@ -178,8 +243,11 @@ def request (config : Config) (problem : Problem) : Http.Request where
   maxBodyBytes := config.maxBodyBytes
   maxRequestBodyBytes := config.maxBodyBytes
 
-def submit (config : Config) (problem : Problem) :
-  IO (Except Http.Error Http.Response) := do
+def submit
+    (config : Config)
+    (problem : Problem)
+    : IO (Except Http.Error Http.Response)
+    := do
   let label := String.intercalate ", " (labels config).toList
   let request := request config problem
   let artifacts ← OATP.Artifacts.start s!"online {label}" problem
@@ -196,10 +264,19 @@ def submit (config : Config) (problem : Problem) :
         OATP.Artifacts.write run "response.error" (Http.Error.message error)
   pure response
 
-private def tagStarts (needle : String) (tag : String) : Bool :=
+private
+def tagStarts
+    (needle : String)
+    (tag : String)
+    : Bool
+    :=
   tag.toLower.startsWith needle
 
-private def bodyText (parts : List HtmlPart) : String :=
+private
+def bodyText
+    (parts : List HtmlPart)
+    : String
+    :=
   let hasBody := parts.any fun part => match part with
     | .tag tag => tagStarts "<body" tag
     | .text _ => false
@@ -219,11 +296,18 @@ private def bodyText (parts : List HtmlPart) : String :=
             else collect inside rest
   String.intercalate "" (collect (!hasBody) parts)
 
-private def decodeHtmlEntities (value : String) : String :=
+private
+def decodeHtmlEntities
+    (value : String)
+    : String
+    :=
   value.replace "&gt;" ">" |>.replace "&lt;" "<" |>.replace "&amp;" "&"
     |>.replace "&quot;" "\"" |>.replace "&#39;" "'"
 
-def parseResponseText (body : String) : Except Grip.ParseError String :=
+def parseResponseText
+    (body : String)
+    : Except Grip.ParseError String
+    :=
   let body := body.trimAscii.toString
   if !body.startsWith "<!DOCTYPE" && !body.toLower.startsWith "<html" then
     .ok body
@@ -232,23 +316,36 @@ def parseResponseText (body : String) : Except Grip.ParseError String :=
     | .error error => .error error
     | .ok parts => .ok <| decodeHtmlEntities (bodyText parts).trimAscii.toString
 
-def responseText (body : String) : String :=
+def responseText
+    (body : String)
+    : String
+    :=
   match parseResponseText body with
   | .ok text => text
   | .error _ => body
 
-def catalogueRequest (endpoint : String) : Http.Request where
+def catalogueRequest
+    (endpoint : String)
+    : Http.Request
+    where
   method := .get
   url := if endpoint == defaultEndpoint then defaultCatalogueEndpoint else endpoint
   maxSeconds := defaultCatalogueTimeoutSeconds
   maxBodyBytes := defaultCatalogueMaxBodyBytes
   maxRequestBodyBytes := defaultCatalogueMaxBodyBytes
 
-def fetchCatalogue (endpoint : String) : IO (Except Http.Error Http.Response) :=
+def fetchCatalogue
+    (endpoint : String)
+    : IO (Except Http.Error Http.Response)
+    :=
   Http.requestWithTransport (catalogueRequest endpoint)
 
-def parseResponse (config : Config) (problem : Problem) (response : Http.Response) :
-    Except ResponseError Artifact := do
+def parseResponse
+    (config : Config)
+    (problem : Problem)
+    (response : Http.Response)
+    : Except ResponseError Artifact
+    := do
   if response.statusCode < 200 || response.statusCode ≥ 300 then
     throw (.httpStatus response.statusCode)
   let token ← match SZSStatus.tokenFromOutput response.body with
diff --git a/OATP/TPTP.lean b/OATP/TPTP.lean
index 32d0a27..f646783 100644
--- a/OATP/TPTP.lean
+++ b/OATP/TPTP.lean
@@ -33,15 +33,24 @@ def defaultTheory : String := supportedTheories.headD "fof"
 
 def theoryChoices : List String := supportedTheories ++ theoryAliases.map Prod.fst
 
-def normalizeTheory (value : String) : Option String :=
+def normalizeTheory
+    (value : String)
+    : Option String
+    :=
   let value := value.toLower
   if value ∈ supportedTheories then some value
   else theoryAliases.find? (·.1 == value) |>.map Prod.snd
 
-def parse (source : String) : Except Grip.ParseError Document :=
+def parse
+    (source : String)
+    : Except Grip.ParseError Document
+    :=
   _root_.TPTP.parseString source
 
-def parseStatement (source : String) : Except Grip.ParseError Statement :=
+def parseStatement
+    (source : String)
+    : Except Grip.ParseError Statement
+    :=
   _root_.TPTP.parseStatementString source
 
 namespace Syntax
@@ -49,15 +58,22 @@ namespace Syntax
 abbrev Term := _root_.TPTP.Formula.Term
 abbrev Formula := _root_.TPTP.Formula.Expr
 
-def parseFormula (source : String) : Except Grip.ParseError Formula :=
+def parseFormula
+    (source : String)
+    : Except Grip.ParseError Formula
+    :=
   _root_.TPTP.Formula.parseFormulaString source
 
 end Syntax
 
 namespace Statement
 
-def ofFof (name : String) (role : Role) (formula : _root_.TPTP.Formula.Expr) :
-    Except String _root_.TPTP.Statement := do
+def ofFof
+    (name : String)
+    (role : Role)
+    (formula : _root_.TPTP.Formula.Expr)
+    : Except String _root_.TPTP.Statement
+    := do
   let formula ← formula.toTPTP
   pure {
     kind := .fof
@@ -66,8 +82,10 @@ def ofFof (name : String) (role : Role) (formula : _root_.TPTP.Formula.Expr) :
     formula
   }
 
-def parseFormula (statement : _root_.TPTP.Statement) :
-    Except Grip.ParseError _root_.TPTP.Formula.Expr :=
+def parseFormula
+    (statement : _root_.TPTP.Statement)
+    : Except Grip.ParseError _root_.TPTP.Formula.Expr
+    :=
   _root_.TPTP.Statement.parseFormula statement
 
 end Statement
@@ -76,7 +94,11 @@ end OATP.TPTP
 
 namespace OATP
 
-def Problem.ofStatement (name : String) (statement : _root_.TPTP.Statement) : Problem where
+def Problem.ofStatement
+    (name : String)
+    (statement : _root_.TPTP.Statement)
+    : Problem
+    where
   name := name
   source := _root_.TPTP.Statement.render statement
 
diff --git a/OATP/Term.lean b/OATP/Term.lean
index 00914ed..055f38a 100644
--- a/OATP/Term.lean
+++ b/OATP/Term.lean
@@ -16,7 +16,9 @@ namespace OATP.Term
 
 open OATP TermColor
 
-def eventText : SearchEvent → Text
+def eventText
+    : SearchEvent →
+      Text
   | .goal snapshot =>
       let context := if snapshot.context.isEmpty then "" else
         "\n" ++ String.intercalate "\n" (snapshot.context.toList.map (fun line => "  " ++ line))
@@ -28,10 +30,16 @@ def eventText : SearchEvent → Text
   | .result outcome => Text.styled "result: " Style.bold ++ Text.plain outcome.status
   | .note message => Text.styled "note: " Style.dim ++ Text.plain message
 
-def renderPlain (events : Array SearchEvent) : String :=
+def renderPlain
+    (events : Array SearchEvent)
+    : String
+    :=
   String.intercalate "\n" (events.toList.map (fun event => (eventText event).plainText))
 
-def renderAnsi16 (events : Array SearchEvent) : String :=
+def renderAnsi16
+    (events : Array SearchEvent)
+    : String
+    :=
   String.intercalate "\n"
     (events.toList.map (fun event => Text.render RenderTarget.ansi16 (eventText event)))
 
diff --git a/OATP/Translate.lean b/OATP/Translate.lean
index 4e05af0..c367074 100644
--- a/OATP/Translate.lean
+++ b/OATP/Translate.lean
@@ -28,24 +28,40 @@ structure GoalTranslation where
   target : String
   deriving Repr
 
-private def hexDigit (value : Nat) : Char :=
+private
+def hexDigit
+    (value : Nat)
+    : Char
+    :=
   if value < 10 then Char.ofNat (48 + value) else Char.ofNat (97 + (value - 10))
 
-private def symbolName (raw : String) : String :=
+private
+def symbolName
+    (raw : String)
+    : String
+    :=
   let body := raw.toUTF8.toList.map fun byte =>
     let value := byte.toNat
     s!"{hexDigit (value / 16)}{hexDigit (value % 16)}"
   "oatp_" ++ if body.isEmpty then "atom" else String.intercalate "" body
 
-private def unsupported (expression : Expr) : MetaM (Except String TPTP.Formula.Expr) := do
+private
+def unsupported
+    (expression : Expr)
+    : MetaM (Except String TPTP.Formula.Expr)
+    := do
   let rendered ← ppExpr expression
   pure <| Except.error (s!"unsupported Lean proposition `{rendered}`; supported fragment is " ++
     "propositional logic over named atoms")
 
 -- partiality: Lean Expr stores recursive applications in arrays; this private MetaM traversal
 -- is conservative and tested at the translation trust boundary.
-private partial def translateProp (expression : Expr) :
-    MetaM (Except String TPTP.Formula.Expr) := do
+private
+partial
+def translateProp
+    (expression : Expr)
+    : MetaM (Except String TPTP.Formula.Expr)
+    := do
   let expression ← instantiateMVars expression
   let (function, arguments) := expression.getAppFnArgs
   if function == ``True && arguments.isEmpty then
@@ -85,15 +101,27 @@ private partial def translateProp (expression : Expr) :
       return ← unsupported expression
   | _ => return ← unsupported expression
 
-private def renderStatement (name : String) (role : _root_.TPTP.Role)
-    (formula : TPTP.Formula.Expr) : Except String String := do
+private
+def renderStatement
+    (name : String)
+    (role : _root_.TPTP.Role)
+    (formula : TPTP.Formula.Expr)
+    : Except String String
+    := do
   let statement ← OATP.TPTP.Statement.ofFof name role formula
   pure <| _root_.TPTP.Statement.render statement
 
-private def renderFormula (formula : TPTP.Formula.Expr) : Except String String :=
+private
+def renderFormula
+    (formula : TPTP.Formula.Expr)
+    : Except String String
+    :=
   formula.toTPTP
 
-def translateGoal (mvarId : MVarId) : MetaM (Except String GoalTranslation) :=
+def translateGoal
+    (mvarId : MVarId)
+    : MetaM (Except String GoalTranslation)
+    :=
   mvarId.withContext do
     let target ← instantiateMVars (← mvarId.getType)
     unless ← isProp target do
diff --git a/examples/Cli.lean b/examples/Cli.lean
index acd953a..594c1b2 100644
--- a/examples/Cli.lean
+++ b/examples/Cli.lean
@@ -25,7 +25,10 @@ structure CliIdentity where
   version : String
   endpoint : String
 
-private def cliIdentity : IO CliIdentity := do
+private
+def cliIdentity
+    : IO CliIdentity
+    := do
   let executable ← Std.IO.Process.getExecutablePath
   let executableName := executable.fileName.getD "tool"
   pure {
@@ -63,7 +66,10 @@ inductive ConfigAction where
   | show
   | path
 
-private def configActionParam : Param ConfigAction :=
+private
+def configActionParam
+    : Param ConfigAction
+    :=
   Param.named "ACTION" (Param.enum [("show", .show), ("path", .path)])
 
 inductive Action where
@@ -75,7 +81,10 @@ inductive Action where
   | repl
   | doctor
 
-def cli (identity : CliIdentity) : Argus.Command Action :=
+def cli
+    (identity : CliIdentity)
+    : Argus.Command Action
+    :=
   Argus.group identity.name
     [ Argus.cmd "run" (Spec.map Action.run RunOptions.spec)
         (description := "Run a local or explicitly selected online portfolio")
@@ -97,11 +106,20 @@ def cli (identity : CliIdentity) : Argus.Command Action :=
 
 private def doctorPalette : ColorScheme := ColorScheme.catppuccin
 
-private def doctorSection (title : String) : IO Unit := do
+private
+def doctorSection
+    (title : String)
+    : IO Unit
+    := do
   writeTextLine Text.empty
   writeTextLine (Text.styled title (Style.bold <+> Style.fg doctorPalette.purple))
 
-private def doctorRow (label value : String) (ok : Bool) : IO Unit := do
+private
+def doctorRow
+    (label value : String)
+    (ok : Bool)
+    : IO Unit
+    := do
   let marker := if ok then
       Text.styled "✓" (Style.bold <+> Style.fg doctorPalette.green)
     else
@@ -112,12 +130,19 @@ private def doctorRow (label value : String) (ok : Bool) : IO Unit := do
   writeTextLine (Text.plain "  " ++ marker ++ Text.plain " " ++ label ++ Text.plain " " ++
     Text.styled value valueStyle)
 
-private def doctorTool (command : String) : IO Unit := do
+private
+def doctorTool
+    (command : String)
+    : IO Unit
+    := do
   match ← Http.commandVersion command with
   | some version => doctorRow command version true
   | none => doctorRow command "not found" false
 
-private def doctorPlatform : IO String := do
+private
+def doctorPlatform
+    : IO String
+    := do
   try
     let output ← IO.Process.output { cmd := "uname", args := #["-s", "-m"] }
     if output.exitCode == 0 then
@@ -131,8 +156,12 @@ private def doctorOnlineProblem : Problem := {
   source := "fof(oatp_doctor, conjecture, (p => p)).\n"
 }
 
-private def doctorOnlineAttempts (endpoint : String)
-    (systems : Array SystemOnTPTP.Catalogue.SystemInfo) : Array Portfolio.Attempt :=
+private
+def doctorOnlineAttempts
+    (endpoint : String)
+    (systems : Array SystemOnTPTP.Catalogue.SystemInfo)
+    : Array Portfolio.Attempt
+    :=
   let timeout := OATP.Runtime.doctorTimeoutSeconds
   let outputLimit := OATP.Runtime.doctorMaxOutputBytes
   systems.map fun system => {
@@ -160,14 +189,20 @@ structure DoctorIssue where
   kind : DoctorIssueKind
   detail : String
 
-private def doctorIssueKindLabel : DoctorIssueKind → String
+private
+def doctorIssueKindLabel
+    : DoctorIssueKind →
+      String
   | .noSZSStatus => "no SZS status"
   | .transportTimeout => "transport timeout"
   | .transportFailure => "transport failure"
   | .httpError => "HTTP error"
   | .requestFailure => "request failed"
 
-private def doctorIssueKind : Portfolio.Failure → DoctorIssueKind
+private
+def doctorIssueKind
+    : Portfolio.Failure →
+      DoctorIssueKind
   | .process _ => .requestFailure
   | .http (.transport message) =>
       if message.contains "timed out" then .transportTimeout else .transportFailure
@@ -177,7 +212,10 @@ private def doctorIssueKind : Portfolio.Failure → DoctorIssueKind
   | .response (.unsupportedStatus _) _ => .requestFailure
   | .response (.malformedBody _) _ => .requestFailure
 
-private def doctorIssue : Portfolio.Result → Option DoctorIssue
+private
+def doctorIssue
+    : Portfolio.Result →
+      Option DoctorIssue
   | .artifact _ _ => none
   | .failed attempt failure =>
       match failure with
@@ -187,11 +225,18 @@ private def doctorIssue : Portfolio.Result → Option DoctorIssue
             failure.message ++ "\n\n" ++ failure.output
           some { prover := attempt.name, kind := doctorIssueKind failure, detail }
 
-private def portfolioName : Portfolio.Result → String
+private
+def portfolioName
+    : Portfolio.Result →
+      String
   | .artifact attempt _ => attempt.name
   | .failed attempt _ => attempt.name
 
-private def doctorIssueSummary (issues : List DoctorIssue) : String :=
+private
+def doctorIssueSummary
+    (issues : List DoctorIssue)
+    : String
+    :=
   let kinds : List DoctorIssueKind :=
     [.noSZSStatus, .transportTimeout, .transportFailure, .httpError, .requestFailure]
   String.intercalate " · " <| kinds.filterMap fun kind =>
@@ -200,7 +245,11 @@ private def doctorIssueSummary (issues : List DoctorIssue) : String :=
 
 private def doctorIssueFile : String := "oatp-doctor-issues.txt"
 
-private def writeDoctorIssues (issues : List DoctorIssue) : IO (Option String) := do
+private
+def writeDoctorIssues
+    (issues : List DoctorIssue)
+    : IO (Option String)
+    := do
   let entries := issues.map fun issue =>
     s!"[{doctorIssueKindLabel issue.kind}] {issue.prover}\n{issue.detail}"
   try
@@ -209,7 +258,11 @@ private def writeDoctorIssues (issues : List DoctorIssue) : IO (Option String) :
     pure (some doctorIssueFile)
   catch _ => pure none
 
-private def printDiagnostic (message : String) : IO UInt32 := do
+private
+def printDiagnostic
+    (message : String)
+    : IO UInt32
+    := do
   let stderr ← IO.getStderr
   let target ← TermColor.targetWithTty .auto (← stderr.isTty)
   let report := (Report.error "command failed").withCode "cli"
@@ -218,10 +271,18 @@ private def printDiagnostic (message : String) : IO UInt32 := do
   stderr.putStr "\n"
   pure 1
 
-private def configProverName (value : String) : String :=
+private
+def configProverName
+    (value : String)
+    : String
+    :=
   OATP.ProverReference.fromPersisted value |>.map OATP.ProverReference.display |>.getD value
 
-private def configSelectedProvers (preferences : OATP.Config.Preferences) : String :=
+private
+def configSelectedProvers
+    (preferences : OATP.Config.Preferences)
+    : String
+    :=
   if !preferences.proverSelectionSet then
     "automatic"
   else if preferences.enabledProvers.isEmpty then
@@ -229,7 +290,12 @@ private def configSelectedProvers (preferences : OATP.Config.Preferences) : Stri
   else
     String.intercalate ", " (preferences.enabledProvers.toList.map configProverName)
 
-private def runConfig (identity : CliIdentity) (action : ConfigAction) : IO UInt32 := do
+private
+def runConfig
+    (identity : CliIdentity)
+    (action : ConfigAction)
+    : IO UInt32
+    := do
   match action with
   | .path =>
       match ← OATP.Config.path with
@@ -259,9 +325,15 @@ private def runConfig (identity : CliIdentity) (action : ConfigAction) : IO UInt
       | none => pure 0
 
     -- partiality: this live UI loop runs until an external IO action sets finished.
-private partial def progressLoop (finished : IO.Ref Bool)
-    (config : Widgets.ProgressConfig) (state : Widgets.IndeterminateProgressState)
-    (region : LiveRegion) : IO Unit := do
+private
+partial
+def progressLoop
+    (finished : IO.Ref Bool)
+    (config : Widgets.ProgressConfig)
+    (state : Widgets.IndeterminateProgressState)
+    (region : LiveRegion)
+    : IO Unit
+    := do
   if ← finished.get then
     let _ ← region.finish
     pure ()
@@ -271,7 +343,13 @@ private partial def progressLoop (finished : IO.Ref Bool)
     IO.sleep 120
     progressLoop finished config state region
 
-private def withProgress {α : Type} (label : String) (action : IO α) : IO α := do
+private
+def withProgress
+    {α : Type}
+    (label : String)
+    (action : IO α)
+    : IO α
+    := do
   if !(← stdoutSupportsControl) then
     return ← action
   withHiddenCursor do
@@ -288,7 +366,11 @@ private def withProgress {α : Type} (label : String) (action : IO α) : IO α :
       let _ ← IO.ofExcept progress.get
     pure result
 
-private def showArtifact (artifact : Artifact) : IO UInt32 := do
+private
+def showArtifact
+    (artifact : Artifact)
+    : IO UInt32
+    := do
   let marker := if SZSStatus.isSuccess artifact.status then "✓" else "!"
   IO.eprintln s!"{marker} {artifact.prover.label}: {artifact.status} ({artifact.elapsedMs}ms)"
   unless artifact.stdout.isEmpty || artifact.stdout.trimAscii.toString.startsWith "<!DOCTYPE" do
@@ -296,14 +378,23 @@ private def showArtifact (artifact : Artifact) : IO UInt32 := do
   unless artifact.stderr.isEmpty do IO.eprint artifact.stderr
   pure <| if SZSStatus.isSuccess artifact.status then 0 else 1
 
-private def processErrorMessage (toolName executable : String) : OATP.Process.Error → String
+private
+def processErrorMessage
+    (toolName executable : String)
+    : OATP.Process.Error →
+      String
   | .io message =>
       s!"could not start local prover `{executable}`: {message}; " ++
         s!"check the path or run `{toolName} doctor`"
   | .outputTooLarge actual limit =>
       s!"local prover output exceeded {limit} bytes ({actual} captured)"
 
-private def runLocal (toolName : String) (options : LocalOptions) : IO UInt32 := do
+private
+def runLocal
+    (toolName : String)
+    (options : LocalOptions)
+    : IO UInt32
+    := do
   try
     let problem ← readProblem options.problem
     let limits : Limits := {
@@ -320,18 +411,27 @@ private def runLocal (toolName : String) (options : LocalOptions) : IO UInt32 :=
     | .error error => printDiagnostic (processErrorMessage toolName options.executable error)
   catch error => printDiagnostic s!"could not read problem: {error}"
 
-private def noLocalProverMessage : IO String := do
+private
+def noLocalProverMessage
+    : IO String
+    := do
   let candidates ← localProverCandidates
   pure <| s!"no local ATP found; tried {String.intercalate ", " candidates.toList}. " ++
     "Install one, pass --prover PATH, or explicitly select an online-* prover"
 
-private def responseErrorMessage : SystemOnTPTP.ResponseError → String
+private
+def responseErrorMessage
+    : SystemOnTPTP.ResponseError →
+      String
   | .httpStatus status => s!"SystemOnTPTP returned HTTP {status}"
   | .missingStatus => "SystemOnTPTP response did not contain an SZS status"
   | .unsupportedStatus status => s!"SystemOnTPTP returned unsupported SZS status `{status}`"
   | .malformedBody message => s!"SystemOnTPTP response was not valid HTML: {message}"
 
-private def showPortfolioResult : Portfolio.Result → IO Bool
+private
+def showPortfolioResult
+    : Portfolio.Result →
+      IO Bool
   | .artifact _ artifact => do
       let marker := if SZSStatus.isSuccess artifact.status then "✓" else "!"
       IO.eprintln s!"{marker} {artifact.prover.label}: {artifact.status} ({artifact.elapsedMs}ms)"
@@ -347,8 +447,13 @@ private def showPortfolioResult : Portfolio.Result → IO Bool
       unless failure.output.isEmpty do IO.eprint failure.output
       pure false
 
-private def portfolioView (total : Nat) (progress : Widgets.IndeterminateProgressState)
-    (results : List Portfolio.Result) : Text :=
+private
+def portfolioView
+    (total : Nat)
+    (progress : Widgets.IndeterminateProgressState)
+    (results : List Portfolio.Result)
+    : Text
+    :=
   let latest := match results.getLast? with
     | some result => s!" · latest {portfolioName result}"
     | none => ""
@@ -361,10 +466,16 @@ private def portfolioView (total : Nat) (progress : Widgets.IndeterminateProgres
   } { progress with label := Text.styled label (Style.fg doctorPalette.foreground) }
 
 -- partiality: this live UI loop runs until an external portfolio action sets finished.
-private partial def portfolioProgressLoop (finished : IO.Ref Bool)
+private
+partial
+def portfolioProgressLoop
+    (finished : IO.Ref Bool)
     (progress : IO.Ref Widgets.IndeterminateProgressState)
-    (results : IO.Ref (List Portfolio.Result)) (region : IO.Ref LiveRegion)
-    (total : Nat) : IO Unit := do
+    (results : IO.Ref (List Portfolio.Result))
+    (region : IO.Ref LiveRegion)
+    (total : Nat)
+    : IO Unit
+    := do
   if ← finished.get then
     pure ()
   else
@@ -378,8 +489,13 @@ private partial def portfolioProgressLoop (finished : IO.Ref Bool)
     IO.sleep 120
     portfolioProgressLoop finished progress results region total
 
-private def withPortfolioProgress {α : Type} (total : Nat)
-    (action : (Portfolio.Result → IO Unit) → IO α) : IO α := do
+private
+def withPortfolioProgress
+    {α : Type}
+    (total : Nat)
+    (action : (Portfolio.Result → IO Unit) → IO α)
+    : IO α
+    := do
   if !(← stdoutSupportsControl) then
     return ← action (fun _ => pure ())
   withHiddenCursor do
@@ -408,7 +524,12 @@ private def withPortfolioProgress {α : Type} (total : Nat)
       let _ ← next.finish
     pure value
 
-private def runDoctorOnline (identity : CliIdentity) (transports : Array String) : IO Bool := do
+private
+def runDoctorOnline
+    (identity : CliIdentity)
+    (transports : Array String)
+    : IO Bool
+    := do
   doctorSection "ONLINE ATP (probe)"
   if transports.isEmpty then
     doctorRow "service" "unavailable (no HTTP transport)" false
@@ -439,7 +560,11 @@ private def runDoctorOnline (identity : CliIdentity) (transports : Array String)
           | none => doctorRow "details" "could not write issue report" false
         pure (responsive > 0)
 
-private def runDoctor (identity : CliIdentity) : IO UInt32 := do
+private
+def runDoctor
+    (identity : CliIdentity)
+    : IO UInt32
+    := do
   let transports ← Http.availableTransports
   let (online, ready) :=
     if transports.contains "curl" then
@@ -466,7 +591,12 @@ private def runDoctor (identity : CliIdentity) : IO UInt32 := do
 
   pure <| if transports.isEmpty || !onlineWorking then 1 else 0
 
-private def runPortfolio (problem : Problem) (attempts : Array Portfolio.Attempt) : IO UInt32 := do
+private
+def runPortfolio
+    (problem : Problem)
+    (attempts : Array Portfolio.Attempt)
+    : IO UInt32
+    := do
   let results ← withPortfolioProgress attempts.size fun onResult =>
     Portfolio.runWith problem attempts onResult
   let mut success := false
@@ -474,7 +604,12 @@ private def runPortfolio (problem : Problem) (attempts : Array Portfolio.Attempt
     success := (← showPortfolioResult result) || success
   pure <| if success then 0 else 1
 
-private def runDefault (identity : CliIdentity) (options : RunOptions) : IO UInt32 := do
+private
+def runDefault
+    (identity : CliIdentity)
+    (options : RunOptions)
+    : IO UInt32
+    := do
   try
     let problem ← readProblem options.problem
     let rawReferences ← if options.provers.isEmpty then
@@ -536,7 +671,12 @@ private def runDefault (identity : CliIdentity) (options : RunOptions) : IO UInt
     else runPortfolio problem attempts
   catch error => printDiagnostic s!"could not read problem: {error}"
 
-private def runSystems (identity : CliIdentity) (options : SystemsOptions) : IO UInt32 := do
+private
+def runSystems
+    (identity : CliIdentity)
+    (options : SystemsOptions)
+    : IO UInt32
+    := do
   writeTextLine (Text.styled s!"{identity.name} systems {identity.version}"
     (Style.bold <+> Style.fg doctorPalette.purple))
   writeTextLine (Text.styled "LOCAL" (Style.bold <+> Style.fg doctorPalette.cyan))
@@ -570,8 +710,14 @@ private def runSystems (identity : CliIdentity) (options : SystemsOptions) : IO
       (Style.fg doctorPalette.comment))
     pure 0
 
-private def submitOnline (options : OnlineOptions) (problem : Problem) (endpoint : String)
-    (system : SystemOnTPTP.Catalogue.SystemInfo) : IO UInt32 := do
+private
+def submitOnline
+    (options : OnlineOptions)
+    (problem : Problem)
+    (endpoint : String)
+    (system : SystemOnTPTP.Catalogue.SystemInfo)
+    : IO UInt32
+    := do
   let config : SystemOnTPTP.Config := {
     systemLabel := system.id
     systemCommands := if system.command.isEmpty then #[] else #[(system.id, system.command)]
@@ -588,7 +734,12 @@ private def submitOnline (options : OnlineOptions) (problem : Problem) (endpoint
       | .error error => printDiagnostic (responseErrorMessage error)
       | .ok artifact => showArtifact { artifact with elapsedMs := (← IO.monoMsNow) - started }
 
-private def runOnline (identity : CliIdentity) (options : OnlineOptions) : IO UInt32 := do
+private
+def runOnline
+    (identity : CliIdentity)
+    (options : OnlineOptions)
+    : IO UInt32
+    := do
   try
     let problem ← readProblem options.problem
     let endpoint := options.remote.endpoint.getD identity.endpoint
@@ -603,7 +754,10 @@ private def runOnline (identity : CliIdentity) (options : OnlineOptions) : IO UI
             s!"run `{identity.name} systems --online`")
   catch error => printDiagnostic s!"could not read problem: {error}"
 
-def main (argv : List String) : IO UInt32 := do
+def main
+    (argv : List String)
+    : IO UInt32
+    := do
   if let "repl" :: replArgs := argv then
     return ← oatpReplMain replArgs
   let identity ← cliIdentity
diff --git a/examples/Demo.lean b/examples/Demo.lean
index 28a80a8..6ab56ef 100644
--- a/examples/Demo.lean
+++ b/examples/Demo.lean
@@ -20,7 +20,9 @@ def sampleEvents : Array SearchEvent := #[
     elapsedMs := 8
   })]
 
-def main : IO Unit := do
+def main
+    : IO Unit
+    := do
   IO.println (OATP.Term.renderPlain sampleEvents)
   IO.println ""
   IO.print (OATP.Term.renderAnsi16 sampleEvents)
diff --git a/examples/ProofDemo.lean b/examples/ProofDemo.lean
index 5305814..b3d3d19 100644
--- a/examples/ProofDemo.lean
+++ b/examples/ProofDemo.lean
@@ -12,7 +12,10 @@ def demoP : Prop := True
 def demoQ : Prop := True
 def demoPredicate (_ : Nat) : Prop := True
 
-private def runProofDemo : TermElabM Unit := do
+private
+def runProofDemo
+    : TermElabM Unit
+    := do
   let goal ← mkFreshExprMVar (some (mkConst ``True))
   match ← OATP.Proof.reconstruct goal.mvarId! .trueIntro with
   | .ok _ => logInfo "OATP proof demo: kernel-checked True introduction"
@@ -68,6 +71,8 @@ meta def elabOATPProofDemo : CommandElab := fun stx =>
 
 #oatp_proof_demo
 
-def main : IO UInt32 := do
+def main
+    : IO UInt32
+    := do
   IO.println "OATP proof demo passed"
   return 0
diff --git a/examples/Repl.lean b/examples/Repl.lean
index 0809c4a..19d19b4 100644
--- a/examples/Repl.lean
+++ b/examples/Repl.lean
@@ -30,9 +30,18 @@ open TermColor.Widgets
 
 private def catalogueNamespace : String := "oatp-repl"
 
-private def appendEntry (app : App) (cell : Nat) (input output : String) (ok : Bool)
-    (elapsedMs : Option Nat := none) (sources : Sources := #[])
-    (diagnostic : Option Diagnostic := none) (report : Option Report := none) : App :=
+private
+def appendEntry
+    (app : App)
+    (cell : Nat)
+    (input output : String)
+    (ok : Bool)
+    (elapsedMs : Option Nat := none)
+    (sources : Sources := #[])
+    (diagnostic : Option Diagnostic := none)
+    (report : Option Report := none)
+    : App
+    :=
   { app with
     entries := { cell, input, output, ok, elapsedMs, sources, diagnostic, report } :: app.entries
     transcriptScroll := 0
@@ -41,7 +50,11 @@ private def appendEntry (app : App) (cell : Nat) (input output : String) (ok : B
 #guard (appendEntry { repl := { history := #["first"] } } 1 "input" "output" true).repl.history ==
   #["first"]
 
-private def diagnosticFor (source message : String) : Source × Diagnostic :=
+private
+def diagnosticFor
+    (source message : String)
+    : Source × Diagnostic
+    :=
   let sourceText := source
   let source := Source.fromBytes "input" source.toUTF8
   let title := message.splitOn "\n" |>.headD message
@@ -49,8 +62,15 @@ private def diagnosticFor (source message : String) : Source × Diagnostic :=
     (Label.primary (Span.range 0 0 sourceText.toUTF8.size))
   (source, diagnostic)
 
-private def note (app : App) (cell : Nat) (input output : String) (ok : Bool)
-    (elapsedMs : Option Nat := none) : App :=
+private
+def note
+    (app : App)
+    (cell : Nat)
+    (input output : String)
+    (ok : Bool)
+    (elapsedMs : Option Nat := none)
+    : App
+    :=
   let (sources, diagnostic) := if ok then
       (#[], none)
     else
@@ -59,8 +79,16 @@ private def note (app : App) (cell : Nat) (input output : String) (ok : Bool)
   appendEntry { app with session := OATP.Repl.note app.session input output } cell input output ok
     elapsedMs sources diagnostic
 
-private def notePlain (app : App) (cell : Nat) (input output : String) (ok : Bool)
-    (elapsedMs : Option Nat := none) (report : Option Report := none) : App :=
+private
+def notePlain
+    (app : App)
+    (cell : Nat)
+    (input output : String)
+    (ok : Bool)
+    (elapsedMs : Option Nat := none)
+    (report : Option Report := none)
+    : App
+    :=
   appendEntry { app with session := OATP.Repl.note app.session input output } cell input output ok
     elapsedMs #[] none report
 
@@ -68,23 +96,41 @@ private def notePlain (app : App) (cell : Nat) (input output : String) (ok : Boo
   | entry :: _ => match entry.diagnostic with | none => true | some _ => false
   | [] => false
 
-private def noteDiagnostic (app : App) (cell : Nat) (input source message : String) : App :=
+private
+def noteDiagnostic
+    (app : App)
+    (cell : Nat)
+    (input source message : String)
+    : App
+    :=
   let (source, diagnostic) := diagnosticFor source message
   appendEntry { app with session := OATP.Repl.note app.session input message }
     cell input message false
     none #[source] (some diagnostic)
 
-private def clearDerived (app : App) : App :=
+private
+def clearDerived
+    (app : App)
+    : App
+    :=
   { app with goal := none, translation := none, term := none, leanGoal := none }
 
-private def invalidateContext (app : App) : App :=
+private
+def invalidateContext
+    (app : App)
+    : App
+    :=
   { clearDerived app with
     runRows := #[]
     runOpen := false
     runFocus := 0
     contextItemFocus := none }
 
-private def clearTranscript (app : App) : App :=
+private
+def clearTranscript
+    (app : App)
+    : App
+    :=
   { app with
     entries := []
     transcriptScroll := 0
@@ -94,17 +140,28 @@ private def clearTranscript (app : App) : App :=
     copyPending := none
     repl := { app.repl with input := {}, historyIndex := none, completion := none } }
 
-private def changesContext (input : String) : Bool :=
+private
+def changesContext
+    (input : String)
+    : Bool
+    :=
   match OATP.Repl.parseInput input with
   | .source _ => true
   | .command command => match command with
       | .parse _ | .axiom _ _ | .conjecture _ _ | .remove _ | .update _ _ | .reset => true
       | _ => false
 
-private def lastHistory (session : OATP.Repl.Session) : String :=
+private
+def lastHistory
+    (session : OATP.Repl.Session)
+    : String
+    :=
   session.history.toList.reverse.head?.map (·.result) |>.getD "ok"
 
-private def artifactText : Portfolio.Result → (String × Bool)
+private
+def artifactText
+    : Portfolio.Result →
+      (String × Bool)
   | .artifact attempt artifact =>
       let head := s!"{attempt.name}: {artifact.status} ({artifact.elapsedMs}ms)"
       let details := if artifact.stderr.contains "no input problem files" then
@@ -118,19 +175,33 @@ private def artifactText : Portfolio.Result → (String × Bool)
       (head ++ details, SZSStatus.isSuccess artifact.status)
   | .failed attempt failure => (s!"{attempt.name}: failed: {failure.message}", false)
 
-private def resultHasIssue : Portfolio.Result → Bool
+private
+def resultHasIssue
+    : Portfolio.Result →
+      Bool
   | .artifact _ artifact => !SZSStatus.isSuccess artifact.status
   | .failed _ _ => true
 
-private def resultSucceeded : Portfolio.Result → Bool
+private
+def resultSucceeded
+    : Portfolio.Result →
+      Bool
   | .artifact _ artifact => SZSStatus.isSuccess artifact.status
   | .failed _ _ => false
 
-private def resultIssueText : Portfolio.Result → String
+private
+def resultIssueText
+    : Portfolio.Result →
+      String
   | .artifact attempt artifact => s!"{attempt.name}: returned {artifact.status}"
   | .failed attempt failure => s!"{attempt.name}: {failure.message}"
 
-private def runReport (strategy : OATP.RunStrategy) (results : List Portfolio.Result) : Report :=
+private
+def runReport
+    (strategy : OATP.RunStrategy)
+    (results : List Portfolio.Result)
+    : Report
+    :=
   let issues := results.filter resultHasIssue
   let report := if strategy == .firstSuccess && results.any resultSucceeded then
       Report.info "first successful prover completed"
@@ -149,10 +220,17 @@ structure RunOutput where
   ok : Bool
   report : Report
 
-private def failedRunOutput (code message : String) : RunOutput :=
+private
+def failedRunOutput
+    (code message : String)
+    : RunOutput
+    :=
   { text := message, ok := false, report := (Report.error message).withCode code }
 
-private def runRow : Portfolio.Result → RunRow
+private
+def runRow
+    : Portfolio.Result →
+      RunRow
   | .artifact attempt artifact =>
       { name := attempt.name
         status := .result artifact.status
@@ -165,14 +243,23 @@ private def runRow : Portfolio.Result → RunRow
   | .failed attempt failure =>
       { name := attempt.name, status := .failed, detail := failure.message }
 
-private def runRowsFor (attempts : Array Portfolio.Attempt) (strategy : OATP.RunStrategy) :
-    Array RunRow :=
+private
+def runRowsFor
+    (attempts : Array Portfolio.Attempt)
+    (strategy : OATP.RunStrategy)
+    : Array RunRow
+    :=
   attempts.mapIdx fun index attempt => {
     name := attempt.name
     status := if strategy == .all || index == 0 then .running else .queued }
 
-private def finishRunRows (rows : Array RunRow) (results : List Portfolio.Result)
-    (strategy : OATP.RunStrategy) : Array RunRow :=
+private
+def finishRunRows
+    (rows : Array RunRow)
+    (results : List Portfolio.Result)
+    (strategy : OATP.RunStrategy)
+    : Array RunRow
+    :=
   let rows := results.foldl (fun rows result =>
     let completed := runRow result
     rows.map fun current => if current.name == completed.name then completed else current) rows
@@ -181,21 +268,38 @@ private def finishRunRows (rows : Array RunRow) (results : List Portfolio.Result
       { row with status := .cancelled, detail := "skipped after first success" } else row
   else rows
 
-private def publishRunRows (app : App) (rows : Array RunRow) : IO Unit := do
+private
+def publishRunRows
+    (app : App)
+    (rows : Array RunRow)
+    : IO Unit
+    := do
   match app.runProgress with
   | some progress => progress.set rows
   | none => pure ()
 
-private def currentRunRows (app : App) : IO (Array RunRow) := do
+private
+def currentRunRows
+    (app : App)
+    : IO (Array RunRow)
+    := do
   match app.runProgress with
   | some progress => progress.get
   | none => pure app.runRows
 
-private def currentProblem (app : App) : Option Problem :=
+private
+def currentProblem
+    (app : App)
+    : Option Problem
+    :=
   app.translation.map (fun source => { name := "lean-goal", source }) |>.orElse
     (fun _ => OATP.Repl.problem app.session)
 
-private def theoryStatus (theory : String) : String :=
+private
+def theoryStatus
+    (theory : String)
+    : String
+    :=
   s!"theory: {theory}; available: {String.intercalate ", " OATP.TPTP.supportedTheories}"
 
 #guard theoryStatus "fof" == "theory: fof; available: fof, cnf, tff"
@@ -209,10 +313,18 @@ private def preferences (app : App) : OATP.Config.Preferences := {
   theme := app.themeName
 }
 
-private def configProverName (value : String) : String :=
+private
+def configProverName
+    (value : String)
+    : String
+    :=
   OATP.ProverReference.fromPersisted value |>.map OATP.ProverReference.display |>.getD value
 
-private def configOutput (app : App) : IO (String × Report) := do
+private
+def configOutput
+    (app : App)
+    : IO (String × Report)
+    := do
   let path := (← OATP.Config.path).map (fun value => s!"{value}") |>.getD "unavailable"
   let (_, warning) ← OATP.Config.load
   let current := preferences app
@@ -249,7 +361,11 @@ private def configOutput (app : App) : IO (String × Report) := do
       | none => []
   pure (output, report)
 
-private def savePreferences (before after : App) : IO App := do
+private
+def savePreferences
+    (before after : App)
+    : IO App
+    := do
   if preferences before == preferences after then
     pure after
   else
@@ -257,23 +373,36 @@ private def savePreferences (before after : App) : IO App := do
     | none => pure after
     | some message => pure { after with statusNotice := some message }
 
-private def installedProverReferences : IO (Array OATP.ProverReference) := do
+private
+def installedProverReferences
+    : IO (Array OATP.ProverReference)
+    := do
   let installed ← OATP.Runtime.installedProvers
   pure (installed.map OATP.ProverReference.fromLocal)
 
-private def onlineProverNames : IO (Except String (Array OATP.ProverReference)) := do
+private
+def onlineProverNames
+    : IO (Except String (Array OATP.ProverReference))
+    := do
   match ← OATP.Runtime.loadCatalogue catalogueNamespace
       SystemOnTPTP.defaultCatalogueEndpoint .normal with
   | .error message => pure (.error message)
   | .ok systems => pure (.ok (systems.map fun system => OATP.ProverReference.fromOnline system.id))
 
-private def selectableProvers : IO (Array OATP.ProverReference × Option String) := do
+private
+def selectableProvers
+    : IO (Array OATP.ProverReference × Option String)
+    := do
   let installed ← installedProverReferences
   match ← onlineProverNames with
   | .ok online => pure (installed ++ online, none)
   | .error message => pure (installed, some message)
 
-private def defaultProvers (app : App) : IO (Array OATP.ProverReference) := do
+private
+def defaultProvers
+    (app : App)
+    : IO (Array OATP.ProverReference)
+    := do
   let installed ← installedProverReferences
   match app.defaultProver with
   | some reference => match reference.kind with
@@ -286,8 +415,12 @@ private def defaultProvers (app : App) : IO (Array OATP.ProverReference) := do
       | some name => pure #[OATP.ProverReference.fromLocal name]
       | none => pure #[]
 
-private def selectedProvers (app : App) (all includeDefault : Bool := false) :
-    IO (Array OATP.ProverReference) := do
+private
+def selectedProvers
+    (app : App)
+    (all includeDefault : Bool := false)
+    : IO (Array OATP.ProverReference)
+    := do
   let installed ← installedProverReferences
   let selected ← if all then
       pure installed
@@ -311,8 +444,13 @@ private def selectedProvers (app : App) (all includeDefault : Bool := false) :
     pure <| defaults.foldl (fun selected reference =>
       if selected.any (· == reference) then selected else selected.push reference) selected
 
-private def runRequest (app : App) (request : OATP.Repl.RunRequest)
-    (includeDefault : Bool := false) : IO RunOutput := do
+private
+def runRequest
+    (app : App)
+    (request : OATP.Repl.RunRequest)
+    (includeDefault : Bool := false)
+    : IO RunOutput
+    := do
   match currentProblem app with
   | none =>
       let message :=
@@ -420,15 +558,22 @@ private def runRequest (app : App) (request : OATP.Repl.RunRequest)
         pure <| RunOutput.mk (String.intercalate "\n" (rendered.map Prod.fst))
           (rendered.any Prod.snd) (runReport app.strategy results.toList)
 
-private def backendLine (input : String) : Bool :=
+private
+def backendLine
+    (input : String)
+    : Bool
+    :=
   match OATP.Repl.parseCommandSpec input with
   | .ok command => match command with
       | .run _ | .local _ | .online _ | .check => true
       | _ => false
   | .error _ => false
 
-private def backendRequest (input : String) :
-    Except String (OATP.Repl.RunRequest × Bool) :=
+private
+def backendRequest
+    (input : String)
+    : Except String (OATP.Repl.RunRequest × Bool)
+    :=
   match OATP.Repl.parseCommandSpec input with
   | .ok (.run request) => pure (request, false)
   | .ok (.local request) => pure ({
@@ -445,7 +590,11 @@ private def backendRequest (input : String) :
   | .ok _ => .error "not a prover command"
   | .error message => .error message
 
-private def startingRunRows (input : String) : Array RunRow :=
+private
+def startingRunRows
+    (input : String)
+    : Array RunRow
+    :=
   match backendRequest input with
   | .ok (request, includeDefault) =>
       if request.references.isEmpty then #[{ name := if includeDefault then
@@ -454,7 +603,10 @@ private def startingRunRows (input : String) : Array RunRow :=
         { name := OATP.ProverReference.display reference, status := .running }
   | .error _ => #[{ name := "run", status := .running }]
 
-private def backgroundJobs : TermColor.Repl.Terminal.JobConfig App where
+private
+def backgroundJobs
+    : TermColor.Repl.Terminal.JobConfig App
+    where
   shouldRun := fun app input => !app.busy && backendLine input
   start := fun app input => { app with
     busy := true
@@ -511,7 +663,11 @@ private def backgroundJobs : TermColor.Repl.Terminal.JobConfig App where
 #guard (backgroundJobs.start { repl := { history := #["first"] } } "/help").repl.history ==
   #["first"]
 
-private def systemsText (request : OATP.Repl.SystemsRequest) : IO String := do
+private
+def systemsText
+    (request : OATP.Repl.SystemsRequest)
+    : IO String
+    := do
   let installed ← OATP.Runtime.installedProvers
   let lines := if installed.isEmpty then ["LOCAL: none"] else
       ["LOCAL:"] ++ installed.toList.map (fun prover => "  " ++ prover)
@@ -528,7 +684,10 @@ private def systemsText (request : OATP.Repl.SystemsRequest) : IO String := do
         pure <| String.intercalate "\n" (lines ++ ["ONLINE:"] ++
           systems.toList.map (fun system => "  " ++ SystemOnTPTP.onlineReference system.id))
 
-private def doctorText : IO String := do
+private
+def doctorText
+    : IO String
+    := do
   let transports ← Http.availableTransports
   let installed ← OATP.Runtime.installedProvers
   let platform ← try
@@ -558,15 +717,30 @@ private def doctorText : IO String := do
     "Use /systems --online to inspect the remote catalogue."
   ]
 
-private def fuzzy (query : String) (value : String) : Bool :=
+private
+def fuzzy
+    (query : String)
+    (value : String)
+    : Bool
+    :=
   let query := query.toLower
   let value := value.toLower
   value == query || value.startsWith query || value.contains query
 
-private def proverMatches (query : String) (reference : OATP.ProverReference) : Bool :=
+private
+def proverMatches
+    (query : String)
+    (reference : OATP.ProverReference)
+    : Bool
+    :=
   fuzzy query (OATP.ProverReference.display reference) || fuzzy query reference.name
 
-private def infoText (app : App) (query : String) : IO (String × Bool) := do
+private
+def infoText
+    (app : App)
+    (query : String)
+    : IO (String × Bool)
+    := do
   let installed ← OATP.Runtime.installedProvers
   let found := installed.filter (fuzzy query)
   if found.size == 1 then
@@ -615,7 +789,11 @@ private def infoText (app : App) (query : String) : IO (String × Bool) := do
           String.intercalate ", " (online.toList.map (fun system =>
             SystemOnTPTP.onlineReference system.id))}", false)
 
-private partial def parseStepTokens : List String → Except String (OATP.Proof.Step × List String)
+private
+partial
+def parseStepTokens
+    : List String →
+      Except String (OATP.Proof.Step × List String)
   | "true-intro" :: rest => pure (.trueIntro, rest)
   | "exact" :: [] => .error "exact expects a hypothesis name"
   | "exact" :: name :: rest => pure (.exact (Name.mkSimple name), rest)
@@ -636,13 +814,23 @@ private partial def parseStepTokens : List String → Except String (OATP.Proof.
   | [] => .error "expected a proof step"
   | token :: _ => .error s!"unknown proof step `{token}`"
 
-private def parseStep (source : String) : Except String OATP.Proof.Step := do
+private
+def parseStep
+    (source : String)
+    : Except String OATP.Proof.Step
+    := do
   let (step, rest) ← parseStepTokens (OATP.Repl.splitWords source)
   match rest with
   | [] => pure step
   | token :: _ => .error s!"unexpected proof step token `{token}`"
 
-private def submitGoal (app : App) (cell : Nat) (input formula : String) : IO App := do
+private
+def submitGoal
+    (app : App)
+    (cell : Nat)
+    (input formula : String)
+    : IO App
+    := do
   let runtime ← match app.leanRuntime with
     | some runtime => pure runtime
     | none => OATP.Lean.Repl.create
@@ -659,8 +847,14 @@ private def submitGoal (app : App) (cell : Nat) (input formula : String) : IO Ap
         translation := none
         term := none } cell input output true
 
-private def submitTheoryFormula (app : App) (cell : Nat) (input : String)
-    (command : OATP.Repl.Command) : IO (Option App) := do
+private
+def submitTheoryFormula
+    (app : App)
+    (cell : Nat)
+    (input : String)
+    (command : OATP.Repl.Command)
+    : IO (Option App)
+    := do
   match command with
   | .axiom name formula | .conjecture name formula =>
       let role := match command with | .axiom _ _ => "axiom" | _ => "conjecture"
@@ -671,8 +865,14 @@ private def submitTheoryFormula (app : App) (cell : Nat) (input : String)
       | .error message => pure (some (note app cell input message false))
   | _ => pure none
 
-private def submitLeanCommand (app : App) (cell : Nat) (input : String)
-    (command : OATP.Repl.Command) : IO (Option App) := do
+private
+def submitLeanCommand
+    (app : App)
+    (cell : Nat)
+    (input : String)
+    (command : OATP.Repl.Command)
+    : IO (Option App)
+    := do
   match command with
   | .goal formula | .toLean formula => do
       return some (← submitGoal app cell input formula)
@@ -715,7 +915,13 @@ private def submitLeanCommand (app : App) (cell : Nat) (input : String)
     | none => return some (note app cell input "no rendered term" false)
   | _ => pure none
 
-private def applyPureCommand (app : App) (cell : Nat) (input : String) : IO App := do
+private
+def applyPureCommand
+    (app : App)
+    (cell : Nat)
+    (input : String)
+    : IO App
+    := do
   match OATP.Repl.apply app.session input with
   | .ok session =>
       let app := if changesContext input then invalidateContext { app with session }
@@ -726,8 +932,14 @@ private def applyPureCommand (app : App) (cell : Nat) (input : String) : IO App
         pure <| appendEntry app cell input (lastHistory session) true
   | .error message => pure (note app cell input message false)
 
-private def submitCommand (app : App) (cell : Nat) (input : String)
-    (command : OATP.Repl.Command) : IO App := do
+private
+def submitCommand
+    (app : App)
+    (cell : Nat)
+    (input : String)
+    (command : OATP.Repl.Command)
+    : IO App
+    := do
   match command with
   | .quit => pure { app with running := false }
   | .load path => do
@@ -875,7 +1087,12 @@ private def submitCommand (app : App) (cell : Nat) (input : String)
       pure (notePlain app cell input result.text result.ok none (some result.report))
   | _ => applyPureCommand app cell input
 
-private def submitCore (app : App) (input : String) : IO App := do
+private
+def submitCore
+    (app : App)
+    (input : String)
+    : IO App
+    := do
   let input := input.trimAscii.toString
   let cell := app.session.nextCell
   let firstWord := (OATP.Repl.splitWords input).headD ""
@@ -892,7 +1109,12 @@ private def submitCore (app : App) (input : String) : IO App := do
   else
     return (← applyPureCommand app cell input)
 
-private def submit (app : App) (input : String) : IO App := do
+private
+def submit
+    (app : App)
+    (input : String)
+    : IO App
+    := do
   let started ← IO.monoMsNow
   let updated ← submitCore app input
   let updated := clearSelection updated
@@ -902,7 +1124,11 @@ private def submit (app : App) (input : String) : IO App := do
   | entry :: rest => pure { app with entries := { entry with elapsedMs := some elapsedMs } :: rest }
   | [] => pure app
 
-private def commandValues (typeName : String) : IO (List String) := do
+private
+def commandValues
+    (typeName : String)
+    : IO (List String)
+    := do
   match typeName with
   | "TOPIC" => pure (List.eraseDups (OATP.Repl.helpTopics ++ OATP.Repl.commandNames))
   | "FORMAT" | "THEORY" | "STEP" =>
@@ -924,10 +1150,18 @@ private def commandValues (typeName : String) : IO (List String) := do
       pure (localNames.toList ++ online.toList)
   | _ => pure []
 
-private def complete (_app : App) (input : TextInputState) : IO (List Completion) :=
+private
+def complete
+    (_app : App)
+    (input : TextInputState)
+    : IO (List Completion)
+    :=
   completeCommandWith OATP.Repl.commandSpec commandValues input
 
-private def appKeymap : TermColor.Repl.Terminal.AppKeymap App where
+private
+def appKeymap
+    : TermColor.Repl.Terminal.AppKeymap App
+    where
   Action := AppKeyAction
   keymap := Keymap.fromSpecs appBindings
   contexts := fun app =>
@@ -997,7 +1231,13 @@ private def appKeymap : TermColor.Repl.Terminal.AppKeymap App where
 #guard (Keymap.fromSpecs appBindings).resolve [AppContext.keyContext .state] (.char 'e') ==
   some AppKeyAction.prepareUpdateContext
 
-private def handleMouse (app : App) (size : Size) (mouse : MouseEvent) : Option App :=
+private
+def handleMouse
+    (app : App)
+    (size : Size)
+    (mouse : MouseEvent)
+    : Option App
+    :=
   if app.runOpen then
     match drawerWidths size.columns with
     | none => none
@@ -1142,7 +1382,11 @@ private def reportTestApp : App := {
   | some app => app.transcriptScroll == 3 && app.panelFocus == .main
   | none => false
 
-private def interactive (initial : App) : IO Unit := do
+private
+def interactive
+    (initial : App)
+    : IO Unit
+    := do
   withAlternateScreen do
     clearScreen
     TermColor.Repl.Terminal.run {
@@ -1164,7 +1408,12 @@ private def interactive (initial : App) : IO Unit := do
       quit := fun app => { app with running := false }
     }
 
-private def runScript (app : App) (lines : List String) : IO App := do
+private
+def runScript
+    (app : App)
+    (lines : List String)
+    : IO App
+    := do
   let mut app := app
   for line in lines do
     if app.running then
@@ -1172,24 +1421,39 @@ private def runScript (app : App) (lines : List String) : IO App := do
         app ← submit app line
   pure app
 
-private def staticOutput (app : App) : IO Unit := do
+private
+def staticOutput
+    (app : App)
+    : IO Unit
+    := do
   for entry in app.entries.reverse do
     IO.println s!"[{entry.cell}] › {entry.input}"
     let timing := entry.elapsedMs.map (fun milliseconds =>
       s!" ({formatElapsed milliseconds})") |>.getD ""
     IO.println s!"    {(if entry.ok then "=" else "!")} {entry.output}{timing}"
 
-private def usage : String :=
+private
+def usage
+    : String
+    :=
   "oatp repl — interactive theorem-proving workbench\n\n" ++
   "usage:\n  lake exe oatp repl\n  lake exe oatp repl --script FILE\n\n" ++
   "examples:\n  /load problem.p\n  /to-lean p => p\n  /snapshot\n  " ++
   "/to-tptp\n  " ++
   "/reconstruct implication-intro h exact h\n  /term"
 
-private def scriptExitCode (app : App) : UInt32 :=
+private
+def scriptExitCode
+    (app : App)
+    : UInt32
+    :=
   if app.entries.all (·.ok) then 0 else 1
 
-private def initialApp (runtime : OATP.Lean.Repl.Runtime) : IO App := do
+private
+def initialApp
+    (runtime : OATP.Lean.Repl.Runtime)
+    : IO App
+    := do
   let (prefs, warning) ← OATP.Config.load
   let runProgress ← IO.mkRef (#[] : Array RunRow)
   let scheme := themeByName prefs.theme |>.getD aurora
@@ -1212,7 +1476,10 @@ private def initialApp (runtime : OATP.Lean.Repl.Runtime) : IO App := do
     statusNotice := warning
   }
 
-def oatpReplMain (args : List String) : IO UInt32 := do
+def oatpReplMain
+    (args : List String)
+    : IO UInt32
+    := do
   if args == ["--help"] || args == ["-h"] then
     IO.println usage
     return 0
diff --git a/test/Tests.lean b/test/Tests.lean
index 302755d..b68104d 100644
--- a/test/Tests.lean
+++ b/test/Tests.lean
@@ -254,13 +254,18 @@ open OATP OATP.TPTP
     { columns := 100, rows := 24 }).plainText.contains "state •"
 #guard (OATP.ReplView.screen { stateOpen := true, panelFocus := .drawer }
     { columns := 100, rows := 24 }).plainText.contains "state • active"
-def completionApp : OATP.ReplView.App :=
+def completionApp
+    : OATP.ReplView.App
+    :=
   { repl := { input := { value := "/st", cursor := 3 }
               completion := some { candidates := #[{ replacement := "/state" }] } } }
 #guard (OATP.ReplView.screen completionApp { columns := 100, rows := 24 }).plainText.contains
   "/state"
 #guard OATP.ReplView.formatElapsed 1_500 == "1.5 s"
-private def timedEntry : OATP.ReplView.TranscriptEntry :=
+private
+def timedEntry
+    : OATP.ReplView.TranscriptEntry
+    :=
   { cell := 1
     input := "/to-lean p => p"
     output := "goal created"
@@ -268,7 +273,10 @@ private def timedEntry : OATP.ReplView.TranscriptEntry :=
 #guard (OATP.ReplView.screen
     { entries := [timedEntry] }
     { columns := 100, rows := 24 }).plainText.contains "(12 ms)"
-private def plainEntry : OATP.ReplView.TranscriptEntry :=
+private
+def plainEntry
+    : OATP.ReplView.TranscriptEntry
+    :=
   { cell := 1
     input := "/to-lean p => p"
     output := "goal created" }
@@ -390,7 +398,9 @@ private def plainEntry : OATP.ReplView.TranscriptEntry :=
   | _ => false
 #guard (OATP.ReplView.clearSelection
     { selectionStart := some (1, 2), selectionEnd := some (3, 4) }).selectionStart.isNone
-def main : IO UInt32 := do
+def main
+    : IO UInt32
+    := do
   let commandCompletions ← TermColor.Repl.completeCommand
     OATP.Repl.commandSpec { value := "/st", cursor := 3 }
   if !(commandCompletions.any (·.replacement == "/state")) then