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

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

instance Lean.instToJsonMessageSeverity : Lean.ToJson Lean.MessageSeverity

instance Lean.instFromJsonMessageSeverity : Lean.FromJson Lean.MessageSeverity

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 : Lean.Name
• openDecls : List Lean.OpenDecl

structure Lean.TraceData : Type

• cls : Lean.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.

• ofFormatWithInfos: Lean.FormatWithInfos → Lean.MessageData

  Eagerly formatted text with info annotations. This constructor is inspected in various hacks.

• ofGoal: Lean.MVarId → Lean.MessageData
• ofWidget: Lean.Widget.WidgetInstance → Lean.MessageData → Lean.MessageData

  A widget instance.

  In ofWidget wi alt, the nested message alt should approximate the contents of the widget without itself using ofWidget wi _. This is used as fallback in environments that cannot display user widgets. alt may nest any structured message, for example ofGoal to approximate a tactic state widget, and, if necessary, even other widget instances (for which approximations are computed recursively).

• 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: Lean.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
• ofLazy: (Option Lean.PPContext → IO Dynamic) → (Lean.MetavarContext → Bool) → Lean.MessageData

  A lazy message. The provided thunk will not be run until it is about to be displayed. This can save computation in cases where the message may never be seen.

  The Dynamic value is expected to be a MessageData, which is a workaround for the positivity restriction.

  If the thunked message is produced for a term that contains a synthetic sorry, hasSyntheticSorry should return true. This is used to filter out certain messages.

instance Lean.instInhabitedMessageData : Inhabited Lean.MessageData

Equations

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

instance Lean.instTypeNameMessageData : TypeName Lean.MessageData

def Lean.MessageData.ofFormat (fmt : Lean.Format) : Lean.MessageData

Eagerly formatted text.

Equations

• Lean.MessageData.ofFormat fmt = Lean.MessageData.ofFormatWithInfos { fmt := fmt, infos := Lean.RBMap.empty }

def Lean.MessageData.lazy (f : Lean.PPContext → IO Lean.MessageData) (hasSyntheticSorry : Lean.MetavarContext → Bool := fun (x : Lean.MetavarContext) => false) : Lean.MessageData

Lazy message data production, with access to the context as given by a surrounding MessageData.withContext (which is expected to exist).

Equations

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

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

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

This does not descend into lazily generated subtrees (.ofLazy); message tags of interest (like those added by logLinter) are expected to be near the root of the MessageData, and not hidden inside .ofLazy.

def Lean.MessageData.kind : Lean.MessageData → Lean.Name

Returns the top-level tag of the message. If none, returns Name.anonymous.

This does not descend into message subtrees (e.g., .compose, .ofLazy). The message kind is expected to describe the whole message.

Equations

• (Lean.MessageData.withContext a msg).kind = msg.kind
• (Lean.MessageData.withNamingContext a msg).kind = msg.kind
• (Lean.MessageData.tagged n a).kind = n
• x.kind = Lean.Name.anonymous

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

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

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

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

Simply formats the name. See MessageData.ofConstName for richer messages.

def Lean.MessageData.ofConstName (constName : Lean.Name) (fullNames : Bool := false) : Lean.MessageData

Represents a constant name such that hovering and "go to definition" works. If there is no such constant in the environment, the name is simply formatted, but sanitized if it is a hygienic name. Use MessageData.ofName if hovers are undesired.

If fullNames is true, then pretty prints as if pp.fullNames is true. Otherwise, pretty prints using the current user setting for pp.fullNames.

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) (ctx? : Option Lean.MessageDataContext := none) : IO Lean.Format

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

instance Lean.MessageData.instAppend : Append Lean.MessageData

Equations

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

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

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

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

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

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

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

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 ∘ Lean.format) l ++ f ++ (Lean.MessageData.ofFormat ∘ Lean.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.

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

• Lean.MessageData.ofList [] = (Lean.MessageData.ofFormat ∘ Lean.format) "[]"
• Lean.MessageData.ofList x = (Lean.MessageData.joinSep x (Lean.MessageData.ofFormat (Std.Format.text ",") ++ Lean.MessageData.ofFormat Lean.Format.line)).sbracket

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

See MessageData.ofList.

Equations

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

def Lean.MessageData.orList (xs : List Lean.MessageData) : Lean.MessageData

Puts MessageData into a comma-separated list with "or" at the back (no Oxford comma). Best used on non-empty lists; returns "– none –" for an empty list.

def Lean.MessageData.andList (xs : List Lean.MessageData) : Lean.MessageData

Puts MessageData into a comma-separated list with "and" at the back (no Oxford comma). Best used on non-empty lists; returns "– none –" for an empty list.

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

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

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} [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} [Lean.ToJson α✝] : Lean.ToJson (Lean.BaseMessage α✝)

Equations

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

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

@[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.

structure Lean.SerialMessageextends Lean.BaseMessage String : 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.

• fileName : String
• pos : Lean.Position
• endPos : Option Lean.Position
• keepFullRange : Bool
• severity : Lean.MessageSeverity
• caption : String
• data : String
• kind : Lean.Name

  The message kind (i.e., the top-level tag).

instance Lean.instToJsonSerialMessage : Lean.ToJson Lean.SerialMessage

Equations

• Lean.instToJsonSerialMessage = { toJson := Lean.toJsonSerialMessage✝ }

instance Lean.instFromJsonSerialMessage : Lean.FromJson Lean.SerialMessage

Equations

• Lean.instFromJsonSerialMessage = { fromJson? := Lean.fromJsonSerialMessage✝ }

@[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 : Bool := false) : String

Equations

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

instance Lean.SerialMessage.instToString : ToString Lean.SerialMessage

@[reducible, inline]

abbrev Lean.Message.kind (msg : Lean.Message) : Lean.Name

Returns the top-level tag of the message. If none, returns Name.anonymous.

This does not descend into message subtrees (e.g., .compose, .ofLazy). The message kind is expected to describe the whole message.

Equations

• msg.kind = msg.data.kind

@[inline]

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

Serializes the message, converting its data into a string and saving its kind.

def Lean.Message.toString (msg : Lean.Message) (includeEndPos : 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.

In the Lean elaborator, we use a fresh message log per command but may also report diagnostics at various points inside a command, which will empty unreported and updated hadErrors accordingly (see CoreM.getAndEmptyMessageLog).

• hadErrors : Bool

  If true, there was an error in the log previously that has already been reported to the user and removed from the log. Thus we say that in the current context (usually the current command), we "have errors" if either this flag is set or there is an error in msgs; see MessageLog.hasErrors. If we have errors, we suppress some error messages that are often the result of a previous error.

• unreported : Lean.PersistentArray Lean.Message

  The list of messages not already reported, in insertion order.

• reportedKinds : Lean.NameSet

  Set of message kinds that have been added to the log. For example, we have the kind unsafe.exponentiation.warning for warning messages associated with the configuration option exponentiation.threshold. We don't produce a warning if the kind is already in the following set.

instance Lean.instInhabitedMessageLog : Inhabited Lean.MessageLog

Equations

• Lean.instInhabitedMessageLog = { default := { hadErrors := default, unreported := default, reportedKinds := default } }

def Lean.MessageLog.empty : Lean.MessageLog

@[deprecated]

def Lean.MessageLog.msgs : Lean.MessageLog → Lean.PersistentArray Lean.Message

Equations

• Lean.MessageLog.msgs = Lean.MessageLog.unreported

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

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

Equations

• Lean.MessageLog.add msg log = { hadErrors := log.hadErrors, unreported := log.unreported.push msg, reportedKinds := log.reportedKinds }

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

instance Lean.MessageLog.instAppend : Append Lean.MessageLog

Equations

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

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

Equations

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

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

Equations

• log.forM f = log.unreported.forM f

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

Converts the unreported messages to a list, oldest message first.

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

Converts the unreported messages to an array, oldest message first.

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

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

  Without context, a MessageData object may be missing information (e.g. hover info) for pretty printing, or may print an error. Hence, addMessageContext should be called on all constructed MessageData (e.g. via m!) before taking it out of context (e.g. leaving MetaM or CoreM).

instance Lean.instAddMessageContextOfMonadLift (m 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

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

class Lean.ToMessageData (α : Type) : Type

• toMessageData : α → Lean.MessageData

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

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

instance Lean.instToMessageDataExpr : Lean.ToMessageData Lean.Expr

Equations

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

instance Lean.instToMessageDataLevel : Lean.ToMessageData Lean.Level

instance Lean.instToMessageDataName : Lean.ToMessageData Lean.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

Equations

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

instance Lean.instToMessageDataMVarId : Lean.ToMessageData Lean.MVarId

Equations

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

@[defaultInstance 1000]

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 α)

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} [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)

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.
• (Lean.KernelException.other msg).toMessageData opts = Lean.toMessageData "(kernel) " ++ Lean.toMessageData msg ++ Lean.toMessageData ""
• Lean.KernelException.deterministicTimeout.toMessageData opts = (Lean.MessageData.ofFormat ∘ Lean.format) "(kernel) deterministic timeout"
• Lean.KernelException.excessiveMemory.toMessageData opts = (Lean.MessageData.ofFormat ∘ Lean.format) "(kernel) excessive memory consumption detected"
• Lean.KernelException.deepRecursion.toMessageData opts = (Lean.MessageData.ofFormat ∘ Lean.format) "(kernel) deep recursion detected"
• Lean.KernelException.interrupted.toMessageData opts = (Lean.MessageData.ofFormat ∘ Lean.format) "(kernel) interrupted"