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

Equations

• One or more equations did not get rendered due to their size.

inductive Lean.MessageSeverity : Type

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

instance Lean.instInhabitedMessageSeverity : Inhabited Lean.MessageSeverity

Equations

• Lean.instInhabitedMessageSeverity = { default := Lean.MessageSeverity.information }

instance Lean.instBEqMessageSeverity : BEq Lean.MessageSeverity

Equations

• Lean.instBEqMessageSeverity = { beq := Lean.beqMessageSeverity✝ }

instance Lean.instToJsonMessageSeverity : Lean.ToJson Lean.MessageSeverity

Equations

• Lean.instToJsonMessageSeverity = { toJson := Lean.toJsonMessageSeverity✝ }

instance Lean.instFromJsonMessageSeverity : Lean.FromJson Lean.MessageSeverity

Equations

• Lean.instFromJsonMessageSeverity = { fromJson? := Lean.fromJsonMessageSeverity✝ }

structure Lean.MessageDataContext : Type

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

structure Lean.NamingContext : Type

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

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

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

structure Lean.PPFormat : Type

Lazily formatted text to be used in MessageData.

• 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.

structure Lean.TraceData : Type

• cls : Lake.Name

  Trace class, e.g. Elab.step.

• startTime : Float

  Start time in seconds; 0 if unknown to avoid Option allocation.

• stopTime : Float

  Stop time in seconds; 0 if unknown to avoid Option allocation.

• collapsed : Bool

  Whether trace node defaults to collapsed in the infoview.

• tag : String

  Optional tag shown in trace.profiler.output output after the trace class name.

inductive Lean.MessageData : Type

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

• 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: Lean.TraceData → Lean.MessageData → Array Lean.MessageData → Lean.MessageData

instance Lean.instInhabitedMessageData : Inhabited Lean.MessageData

Equations

• Lean.instInhabitedMessageData = { default := Lean.MessageData.ofFormat default }

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.

Equations

• Lean.MessageData.nil = Lean.MessageData.ofFormat Lean.Format.nil

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

Equations

• Lean.MessageData.mkPPContext nCtx ctx = { env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts, currNamespace := nCtx.currNamespace, openDecls := nCtx.openDecls }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.MessageData.ofName n = Lean.MessageData.ofFormat (Std.format n)

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

Equations

• msg.hasSyntheticSorry = Lean.MessageData.hasSyntheticSorry.visit none msg

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

Equations

• msgData.format = Lean.MessageData.formatAux { currNamespace := Lean.Name.anonymous, openDecls := [] } none msgData

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

Equations

• msgData.toString = do let __do_lift ← msgData.format pure (toString __do_lift)

instance Lean.MessageData.instAppend : Append Lean.MessageData

Equations

• Lean.MessageData.instAppend = { append := Lean.MessageData.compose }

instance Lean.MessageData.instCoeString : Coe String Lean.MessageData

Equations

• Lean.MessageData.instCoeString = { coe := Lean.MessageData.ofFormat ∘ Std.format }

instance Lean.MessageData.instCoeFormat : Coe Lean.Format Lean.MessageData

Equations

• Lean.MessageData.instCoeFormat = { coe := Lean.MessageData.ofFormat }

instance Lean.MessageData.instCoeLevel : Coe Lean.Level Lean.MessageData

Equations

• Lean.MessageData.instCoeLevel = { coe := Lean.MessageData.ofLevel }

instance Lean.MessageData.instCoeExpr : Coe Lean.Expr Lean.MessageData

Equations

• Lean.MessageData.instCoeExpr = { coe := Lean.MessageData.ofExpr }

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

Equations

• Lean.MessageData.instCoeName = { coe := Lean.MessageData.ofName }

instance Lean.MessageData.instCoeSyntax : Coe Lean.Syntax Lean.MessageData

Equations

• Lean.MessageData.instCoeSyntax = { coe := Lean.MessageData.ofSyntax }

instance Lean.MessageData.instCoeMVarId : Coe Lean.MVarId Lean.MessageData

Equations

• Lean.MessageData.instCoeMVarId = { coe := Lean.MessageData.ofGoal }

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Lean.MessageData.instCoeArrayExpr = { coe := fun (es : Array Lean.Expr) => Lean.MessageData.arrayExpr.toMessageData es 0 ((Lean.MessageData.ofFormat ∘ Std.format) "#[") }

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.

Equations

• Lean.MessageData.bracket l f r = (Lean.MessageData.nest l.length ((Lean.MessageData.ofFormat ∘ Std.format) l ++ f ++ (Lean.MessageData.ofFormat ∘ Std.format) r)).group

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

Wrap the given message in parentheses ().

Equations

• f.paren = Lean.MessageData.bracket "(" f ")"

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

Wrap the given message in square brackets [].

Equations

• f.sbracket = Lean.MessageData.bracket "[" f "]"

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

Append the given list of messages with the given separator.

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.

Equations

• One or more equations did not get rendered due to their size.

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

See MessageData.ofList.

Equations

• Lean.MessageData.ofArray msgs = Lean.MessageData.ofList msgs.toList

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

Equations

• Lean.MessageData.instCoeList = { coe := Lean.MessageData.ofList }

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

Equations

• Lean.MessageData.instCoeListExpr = { coe := fun (es : List Lean.Expr) => Lean.MessageData.ofList (List.map Lean.MessageData.ofExpr es) }

structure Lean.BaseMessage (α : Type u) : Type u

A BaseMessage is a richly formatted piece of information emitted by Lean. They are rendered by client editors in the infoview and in diagnostic windows. There are two varieties in the Lean core:

• Message: Uses structured, effectful MessageData for formatting content.
• SerialMessage: Stores pure String data. Obtained by running the effectful Message.serialize.

• fileName : String
• pos : Lean.Position
• endPos : Option Lean.Position
• keepFullRange : Bool

  If true, report range as given; see msgToInteractiveDiagnostic.

• severity : Lean.MessageSeverity
• caption : String
• data : α

  The content of the message.

instance Lean.instInhabitedBaseMessage : {a : Type u_1} → [inst : Inhabited a] → Inhabited (Lean.BaseMessage a)

Equations

• One or more equations did not get rendered due to their size.

instance Lean.instToJsonBaseMessage : {α : Type u_1} → [inst : Lean.ToJson α] → Lean.ToJson (Lean.BaseMessage α)

Equations

• Lean.instToJsonBaseMessage = { toJson := Lean.toJsonBaseMessage✝ }

instance Lean.instFromJsonBaseMessage : {α : Type} → [inst : Lean.FromJson α] → Lean.FromJson (Lean.BaseMessage α)

Equations

• Lean.instFromJsonBaseMessage = { fromJson? := Lean.fromJsonBaseMessage✝ }

@[reducible, inline]

abbrev Lean.Message : Type

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.

Equations

• Lean.Message = Lean.BaseMessage Lean.MessageData

@[reducible, inline]

abbrev Lean.SerialMessage : Type

A SerialMessage is a Message whose MessageData has been eagerly serialized and is thus appropriate for use in pure contexts where the effectful MessageData.toString cannot be used.

Equations

• Lean.SerialMessage = Lean.BaseMessage String

@[inline]

def Lean.SerialMessage.toMessage (msg : Lean.SerialMessage) : Lean.Message

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

instance Lean.SerialMessage.instToString : ToString Lean.SerialMessage

Equations

• Lean.SerialMessage.instToString = { toString := fun (msg : Lean.SerialMessage) => msg.toString }

@[inline]

def Lean.Message.serialize (msg : Lean.Message) : IO Lean.SerialMessage

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• msg.toString includeEndPos = do let __do_lift ← msg.serialize pure (inline (__do_lift.toString includeEndPos))

def Lean.Message.toJson (msg : Lean.Message) : IO Lean.Json

Equations

• msg.toJson = do let __do_lift ← msg.serialize pure (inline (Lean.toJson __do_lift))

structure Lean.MessageLog : Type

A persistent array of messages.

• msgs : Lean.PersistentArray Lean.Message

instance Lean.instInhabitedMessageLog : Inhabited Lean.MessageLog

Equations

• Lean.instInhabitedMessageLog = { default := { msgs := default } }

def Lean.MessageLog.empty : Lean.MessageLog

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• log.isEmpty = log.msgs.isEmpty

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

Equations

• Lean.MessageLog.add msg log = { msgs := log.msgs.push msg }

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

Equations

• l₁.append l₂ = { msgs := l₁.msgs ++ l₂.msgs }

instance Lean.MessageLog.instAppend : Append Lean.MessageLog

Equations

• Lean.MessageLog.instAppend = { append := Lean.MessageLog.append }

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

Equations

• log.hasErrors = log.msgs.any fun (m : Lean.Message) => match m.severity with | Lean.MessageSeverity.error => true | x => false

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• log.getInfoMessages = { msgs := log.msgs.filter fun (m : Lean.Message) => match m.severity with | Lean.MessageSeverity.information => true | x => false }

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

Equations

• log.forM f = log.msgs.forM f

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

Converts the log to a list, oldest message first.

Equations

• log.toList = log.msgs.toList

def Lean.MessageLog.toArray (log : Lean.MessageLog) : Array Lean.Message

Converts the log to an array, oldest message first.

Equations

• log.toArray = log.msgs.toArray

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

Equations

• msg.nestD = Lean.MessageData.nest 2 msg

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

Equations

• Lean.indentD msg = (Lean.MessageData.ofFormat Lean.Format.line ++ msg).nestD

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

Equations

• Lean.indentExpr e = Lean.indentD (Lean.MessageData.ofExpr e)

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

• addMessageContext : Lean.MessageData → m Lean.MessageData

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

Equations

• Lean.instAddMessageContextOfMonadLift m n = { addMessageContext := fun (msg : Lean.MessageData) => liftM (Lean.addMessageContext msg) }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

class Lean.ToMessageData (α : Type) : Type

• toMessageData : α → Lean.MessageData

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.instToMessageDataOfToFormat = { toMessageData := Lean.MessageData.ofFormat ∘ Std.format }

instance Lean.instToMessageDataExpr : Lean.ToMessageData Lean.Expr

Equations

• Lean.instToMessageDataExpr = { toMessageData := Lean.MessageData.ofExpr }

instance Lean.instToMessageDataLevel : Lean.ToMessageData Lean.Level

Equations

• Lean.instToMessageDataLevel = { toMessageData := Lean.MessageData.ofLevel }

instance Lean.instToMessageDataName : Lean.ToMessageData Lake.Name

Equations

• Lean.instToMessageDataName = { toMessageData := Lean.MessageData.ofName }

instance Lean.instToMessageDataString : Lean.ToMessageData String

Equations

• Lean.instToMessageDataString = { toMessageData := Lean.stringToMessageData }

instance Lean.instToMessageDataSyntax : Lean.ToMessageData Lean.Syntax

Equations

• Lean.instToMessageDataSyntax = { toMessageData := Lean.MessageData.ofSyntax }

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

Equations

• Lean.instToMessageDataTSyntax = { toMessageData := fun (x : Lean.TSyntax k) => Lean.MessageData.ofSyntax x.raw }

instance Lean.instToMessageDataFormat : Lean.ToMessageData Lean.Format

Equations

• Lean.instToMessageDataFormat = { toMessageData := Lean.MessageData.ofFormat }

instance Lean.instToMessageDataMVarId : Lean.ToMessageData Lean.MVarId

Equations

• Lean.instToMessageDataMVarId = { toMessageData := Lean.MessageData.ofGoal }

instance Lean.instToMessageDataMessageData : Lean.ToMessageData Lean.MessageData

Equations

• Lean.instToMessageDataMessageData = { toMessageData := id }

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

Equations

• Lean.instToMessageDataList = { toMessageData := fun (as : List α) => Lean.MessageData.ofList (List.map Lean.toMessageData as) }

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

Equations

• Lean.instToMessageDataArray = { toMessageData := fun (as : Array α) => Lean.toMessageData as.toList }

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

Equations

• Lean.instToMessageDataSubarray = { toMessageData := fun (as : Subarray α) => Lean.toMessageData as.toArray.toList }

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

Equations

• One or more equations did not get rendered due to their size.

instance Lean.instToMessageDataProd {α : Type} {β : Type} [Lean.ToMessageData α] [Lean.ToMessageData β] : Lean.ToMessageData (α × β)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.termM!_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.toMessageList msgs = Lean.indentD (Lean.MessageData.joinSep msgs.toList (Lean.toMessageData "\n\n"))

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

Equations

• One or more equations did not get rendered due to their size.