def Lean.mkErrorStringWithPos (fileName : String) (pos : Lean.Position) (msg : String) (endPos : optParam (Option Lean.Position) none) : String

inductive Lean.MessageSeverity : Type

• information: Lean.MessageSeverity
• warning: Lean.MessageSeverity
• error: Lean.MessageSeverity

instance Lean.instInhabitedMessageSeverity : Inhabited Lean.MessageSeverity

instance Lean.instBEqMessageSeverity : BEq Lean.MessageSeverity

structure Lean.MessageDataContext : Type

• env : Lean.Environment
• mctx : Lean.MetavarContext
• lctx : Lean.LocalContext
• opts : Lean.Options

structure Lean.NamingContext : Type

• currNamespace : Lake.Name
• openDecls : List Lean.OpenDecl

A naming context is the information needed to shorten names in pretty printing.

It gives the current namespace and the list of open declarations.

structure Lean.PPFormat : Type

• pp : Option Lean.PPContext → IO Lean.FormatWithInfos

  Pretty-prints text using surrounding context, if any.

• hasSyntheticSorry : Lean.MetavarContext → Bool

  Searches for synthetic sorries in original input. Used to filter out certain messages.

Lazily formatted text to be used in MessageData.

inductive Lean.MessageData : Type

• ofFormat: Lean.Format → Lean.MessageData

  Eagerly formatted text. We inspect this in various hacks, so it is not immediately subsumed by ofPPFormat.

• ofPPFormat: Lean.PPFormat → Lean.MessageData

  Lazily formatted text.

• ofGoal: Lean.MVarId → Lean.MessageData
• withContext: Lean.MessageDataContext → Lean.MessageData → Lean.MessageData

  withContext ctx d specifies the pretty printing context (env, mctx, lctx, opts) for the nested expressions in d.

• withNamingContext: Lean.NamingContext → Lean.MessageData → Lean.MessageData
• nest: Nat → Lean.MessageData → Lean.MessageData

  Lifted Format.nest

• group: Lean.MessageData → Lean.MessageData

  Lifted Format.group

• compose: Lean.MessageData → Lean.MessageData → Lean.MessageData

  Lifted Format.compose

• tagged: Lake.Name → Lean.MessageData → Lean.MessageData

  Tagged sections. Name should be viewed as a "kind", and is used by MessageData inspector functions. Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure".

• trace: Lake.Name → Lean.MessageData → Array Lean.MessageData → optParam Bool false → Lean.MessageData

Structured message data. We use it for reporting errors, trace messages, etc.

instance Lean.instInhabitedMessageData : Inhabited Lean.MessageData

def Lean.MessageData.isEmpty : Lean.MessageData → Bool

Determines whether the message contains any content.

Equations

• Lean.MessageData.isEmpty (Lean.MessageData.ofFormat f) = Std.Format.isEmpty f
• Lean.MessageData.isEmpty (Lean.MessageData.withContext a m) = Lean.MessageData.isEmpty m
• Lean.MessageData.isEmpty (Lean.MessageData.withNamingContext a m) = Lean.MessageData.isEmpty m
• Lean.MessageData.isEmpty (Lean.MessageData.nest a m) = Lean.MessageData.isEmpty m
• Lean.MessageData.isEmpty (Lean.MessageData.group m) = Lean.MessageData.isEmpty m
• Lean.MessageData.isEmpty (Lean.MessageData.compose m₁ m₂) = (Lean.MessageData.isEmpty m₁ && Lean.MessageData.isEmpty m₂)
• Lean.MessageData.isEmpty (Lean.MessageData.tagged a m) = Lean.MessageData.isEmpty m
• Lean.MessageData.isEmpty x = false

partial def Lean.MessageData.hasTag (p : Lake.Name → Bool) : Lean.MessageData → Bool

Returns true when the message contains a MessageData.tagged tag .. constructor where p tag is true.

def Lean.MessageData.nil : Lean.MessageData

An empty message.

def Lean.MessageData.mkPPContext (nCtx : Lean.NamingContext) (ctx : Lean.MessageDataContext) : Lean.PPContext

def Lean.MessageData.ofSyntax (stx : Lean.Syntax) : Lean.MessageData

def Lean.MessageData.ofExpr (e : Lean.Expr) : Lean.MessageData

def Lean.MessageData.ofLevel (l : Lean.Level) : Lean.MessageData

def Lean.MessageData.ofName (n : Lake.Name) : Lean.MessageData

def Lean.MessageData.hasSyntheticSorry (msg : Lean.MessageData) : Bool

partial def Lean.MessageData.hasSyntheticSorry.visit (mctx? : Option Lean.MetavarContext) : Lean.MessageData → Bool

partial def Lean.MessageData.formatAux : Lean.NamingContext → Option Lean.MessageDataContext → Lean.MessageData → IO Lean.Format

def Lean.MessageData.format (msgData : Lean.MessageData) : IO Lean.Format

def Lean.MessageData.toString (msgData : Lean.MessageData) : IO String

instance Lean.MessageData.instAppendMessageData : Append Lean.MessageData

instance Lean.MessageData.instCoeStringMessageData : Coe String Lean.MessageData

instance Lean.MessageData.instCoeFormatMessageData : Coe Lean.Format Lean.MessageData

instance Lean.MessageData.instCoeLevelMessageData : Coe Lean.Level Lean.MessageData

instance Lean.MessageData.instCoeExprMessageData : Coe Lean.Expr Lean.MessageData

instance Lean.MessageData.instCoeNameMessageData : Coe Lake.Name Lean.MessageData

instance Lean.MessageData.instCoeSyntaxMessageData : Coe Lean.Syntax Lean.MessageData

instance Lean.MessageData.instCoeMVarIdMessageData : Coe Lean.MVarId Lean.MessageData

instance Lean.MessageData.instCoeOptionExprMessageData : Coe (Option Lean.Expr) Lean.MessageData

partial def Lean.MessageData.arrayExpr.toMessageData (es : Array Lean.Expr) (i : Nat) (acc : Lean.MessageData) : Lean.MessageData

instance Lean.MessageData.instCoeArrayExprMessageData : Coe (Array Lean.Expr) Lean.MessageData

def Lean.MessageData.bracket (l : String) (f : Lean.MessageData) (r : String) : Lean.MessageData

Wrap the given message in l and r. See also Format.bracket.

def Lean.MessageData.paren (f : Lean.MessageData) : Lean.MessageData

Wrap the given message in parentheses ().

def Lean.MessageData.sbracket (f : Lean.MessageData) : Lean.MessageData

Wrap the given message in square brackets [].

def Lean.MessageData.joinSep : List Lean.MessageData → Lean.MessageData → Lean.MessageData

Append the given list of messages with the given separarator.

Equations

• Lean.MessageData.joinSep [] x = Lean.MessageData.ofFormat Lean.Format.nil
• Lean.MessageData.joinSep [a] x = a
• Lean.MessageData.joinSep (a :: as) x = a ++ x ++ Lean.MessageData.joinSep as x

def Lean.MessageData.ofList : List Lean.MessageData → Lean.MessageData

Write the given list of messages as a list, separating each item with ,\n and surrounding with square brackets.

def Lean.MessageData.ofArray (msgs : Array Lean.MessageData) : Lean.MessageData

See MessageData.ofList.

instance Lean.MessageData.instCoeListMessageData : Coe (List Lean.MessageData) Lean.MessageData

instance Lean.MessageData.instCoeListExprMessageData : Coe (List Lean.Expr) Lean.MessageData

structure Lean.Message : Type

• fileName : String
• pos : Lean.Position
• endPos : Option Lean.Position
• severity : Lean.MessageSeverity
• caption : String
• data : Lean.MessageData

  The content of the message.

A Message is a richly formatted piece of information emitted by Lean. They are rendered by client editors in the infoview and in diagnostic windows.

instance Lean.instInhabitedMessage : Inhabited Lean.Message

def Lean.Message.toString (msg : Lean.Message) (includeEndPos : optParam Bool false) : IO String

structure Lean.MessageLog : Type

• msgs : Lean.PersistentArray Lean.Message

A persistent array of messages.

instance Lean.instInhabitedMessageLog : Inhabited Lean.MessageLog

def Lean.MessageLog.empty : Lean.MessageLog

def Lean.MessageLog.isEmpty (log : Lean.MessageLog) : Bool

def Lean.MessageLog.add (msg : Lean.Message) (log : Lean.MessageLog) : Lean.MessageLog

def Lean.MessageLog.append (l₁ : Lean.MessageLog) (l₂ : Lean.MessageLog) : Lean.MessageLog

instance Lean.MessageLog.instAppendMessageLog : Append Lean.MessageLog

def Lean.MessageLog.hasErrors (log : Lean.MessageLog) : Bool

def Lean.MessageLog.errorsToWarnings (log : Lean.MessageLog) : Lean.MessageLog

def Lean.MessageLog.getInfoMessages (log : Lean.MessageLog) : Lean.MessageLog

def Lean.MessageLog.forM {m : Type → Type} [Monad m] (log : Lean.MessageLog) (f : Lean.Message → m Unit) : m Unit

def Lean.MessageLog.toList (log : Lean.MessageLog) : List Lean.Message

def Lean.MessageData.nestD (msg : Lean.MessageData) : Lean.MessageData

def Lean.indentD (msg : Lean.MessageData) : Lean.MessageData

def Lean.indentExpr (e : Lean.Expr) : Lean.MessageData

class Lean.AddMessageContext (m : Type → Type) : Type

• addMessageContext : Lean.MessageData → m Lean.MessageData

instance Lean.instAddMessageContext (m : Type → Type) (n : Type → Type) [MonadLift m n] [Lean.AddMessageContext m] : Lean.AddMessageContext n

def Lean.addMessageContextPartial {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadOptions m] (msgData : Lean.MessageData) : m Lean.MessageData

def Lean.addMessageContextFull {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadMCtx m] [Lean.MonadLCtx m] [Lean.MonadOptions m] (msgData : Lean.MessageData) : m Lean.MessageData

class Lean.ToMessageData (α : Type) : Type

• toMessageData : α → Lean.MessageData

def Lean.stringToMessageData (str : String) : Lean.MessageData

instance Lean.instToMessageData {α : Type} [Lean.ToFormat α] : Lean.ToMessageData α

instance Lean.instToMessageDataExpr : Lean.ToMessageData Lean.Expr

instance Lean.instToMessageDataLevel : Lean.ToMessageData Lean.Level

instance Lean.instToMessageDataName : Lean.ToMessageData Lake.Name

instance Lean.instToMessageDataString : Lean.ToMessageData String

instance Lean.instToMessageDataSyntax : Lean.ToMessageData Lean.Syntax

instance Lean.instToMessageDataTSyntax {k : Lean.SyntaxNodeKinds} : Lean.ToMessageData (Lean.TSyntax k)

instance Lean.instToMessageDataFormat : Lean.ToMessageData Lean.Format

instance Lean.instToMessageDataMVarId : Lean.ToMessageData Lean.MVarId

instance Lean.instToMessageDataMessageData : Lean.ToMessageData Lean.MessageData

instance Lean.instToMessageDataList {α : Type} [Lean.ToMessageData α] : Lean.ToMessageData (List α)

instance Lean.instToMessageDataArray {α : Type} [Lean.ToMessageData α] : Lean.ToMessageData (Array α)

instance Lean.instToMessageDataSubarray {α : Type} [Lean.ToMessageData α] : Lean.ToMessageData (Subarray α)

instance Lean.instToMessageDataOption {α : Type} [Lean.ToMessageData α] : Lean.ToMessageData (Option α)

instance Lean.instToMessageDataOptionExpr : Lean.ToMessageData (Option Lean.Expr)

def Lean.termM!_ : Lean.ParserDescr

def Lean.toMessageList (msgs : Array Lean.MessageData) : Lean.MessageData

def Lean.KernelException.toMessageData (e : Lean.KernelException) (opts : Lean.Options) : Lean.MessageData