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

Creates a string describing an error message msg produced at pos, optionally ending at endPos, in fileName.

Additional optional arguments can be used to prepend a label kind describing the severity of the error (e.g., "warning" or "error") and a bracketed name label displaying the name of the error if it has one.

Equations

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

inductive Lean.MessageSeverity : Type

• information : MessageSeverity
• warning : MessageSeverity
• error : MessageSeverity

Instances For

• Lean.instBEqMessageSeverity
• Lean.instFromJsonMessageSeverity
• Lean.instInhabitedMessageSeverity
• Lean.instToJsonMessageSeverity
• Lean.instToStringMessageSeverity

instance Lean.instInhabitedMessageSeverity : Inhabited MessageSeverity

Equations

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

instance Lean.instBEqMessageSeverity : BEq MessageSeverity

Equations

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

instance Lean.instToJsonMessageSeverity : ToJson MessageSeverity

Equations

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

instance Lean.instFromJsonMessageSeverity : FromJson MessageSeverity

Equations

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

def Lean.MessageSeverity.toString : MessageSeverity → String

Equations

• Lean.MessageSeverity.information.toString = "information"
• Lean.MessageSeverity.warning.toString = "warning"
• Lean.MessageSeverity.error.toString = "error"

instance Lean.instToStringMessageSeverity : ToString MessageSeverity

Equations

• Lean.instToStringMessageSeverity = { toString := Lean.MessageSeverity.toString }

structure Lean.MessageDataContext : Type

• env : Environment
• mctx : MetavarContext
• lctx : LocalContext
• opts : 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 : Name
• openDecls : List OpenDecl

structure Lean.TraceData : Type

• cls : 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 : FormatWithInfos → MessageData

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

• ofGoal : MVarId → MessageData
• ofWidget : Widget.WidgetInstance → MessageData → 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).

  Note that unlike with Widget.savePanelWidgetInfo, the infoview will not pass any additional props to the widget instance.

• withContext : MessageDataContext → MessageData → MessageData

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

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

  Lifted Format.nest

• group : MessageData → MessageData

  Lifted Format.group

• compose : MessageData → MessageData → MessageData

  Lifted Format.compose

• tagged : Name → MessageData → 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 (data : TraceData) (msg : MessageData) (children : Array MessageData) : MessageData
• ofLazy (f : Option PPContext → BaseIO Dynamic) (hasSyntheticSorry : MetavarContext → Bool) : 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.

Instances For

• Lean.MessageData.instAppend
• Lean.MessageData.instCoeArrayExpr
• Lean.MessageData.instCoeExpr
• Lean.MessageData.instCoeFormat
• Lean.MessageData.instCoeLevel
• Lean.MessageData.instCoeList
• Lean.MessageData.instCoeListExpr
• Lean.MessageData.instCoeMVarId
• Lean.MessageData.instCoeName
• Lean.MessageData.instCoeOptionExpr
• Lean.MessageData.instCoeString
• Lean.MessageData.instCoeSyntax
• Lean.instInhabitedMessageData
• Lean.instToMessageDataMessageData
• Lean.instTypeNameMessageData
• Qq.instCoeOutQuotedMessageData

instance Lean.instInhabitedMessageData : Inhabited MessageData

Equations

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

instance Lean.instTypeNameMessageData : TypeName MessageData

Equations

• Lean.instTypeNameMessageData = Lean.inst✝

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

Eagerly formatted text.

Equations

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

def Lean.MessageData.lazy (f : PPContext → BaseIO MessageData) (hasSyntheticSorry : MetavarContext → Bool := fun (x : MetavarContext) => false) (onMissingContext : Unit → BaseIO MessageData := fun (x : Unit) => pure (ofFormat (Std.Format.text "(invalid MessageData.lazy, missing context)"))) : 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 : Name → Bool) : 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 : MessageData → 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.isTrace : MessageData → Bool

Equations

• (Lean.MessageData.withContext a msg).isTrace = msg.isTrace
• (Lean.MessageData.withNamingContext a msg).isTrace = msg.isTrace
• (Lean.MessageData.tagged a msg).isTrace = msg.isTrace
• (Lean.MessageData.trace data msg children).isTrace = true
• x✝.isTrace = false

def Lean.MessageData.composePreservingKind : MessageData → MessageData → MessageData

composePreservingKind msg msg' appends the contents of msg' to the end of msg but ensures that the resulting message preserves the kind (as given by MessageData.kind) of msg.

Equations

• (Lean.MessageData.withContext ctx msg).composePreservingKind x✝ = Lean.MessageData.withContext ctx (msg.composePreservingKind x✝)
• (Lean.MessageData.withNamingContext nc msg).composePreservingKind x✝ = Lean.MessageData.withNamingContext nc (msg.composePreservingKind x✝)
• (Lean.MessageData.tagged t msg).composePreservingKind x✝ = Lean.MessageData.tagged t (msg.compose x✝)
• x✝¹.composePreservingKind x✝ = x✝¹.compose x✝

def Lean.MessageData.nil : MessageData

An empty message.

Equations

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

def Lean.MessageData.mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : 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 : Syntax) : MessageData

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

def Lean.MessageData.ofConstName (constName : Name) (fullNames : Bool := false) : 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.

Equations

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

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

Equations

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

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

opaque Lean.MessageData.maxTraceChildren : Lean.Option Nat

Maximum number of trace node children to display by default to prevent slowdowns from rendering. In the info view, more children can be expanded interactively.

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

def Lean.MessageData.format (msgData : MessageData) (ctx? : Option MessageDataContext := none) : BaseIO Format

Equations

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

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

Equations

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

instance Lean.MessageData.instAppend : Append MessageData

Equations

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

instance Lean.MessageData.instCoeString : Coe String MessageData

Equations

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

instance Lean.MessageData.instCoeFormat : Coe Format MessageData

Equations

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

instance Lean.MessageData.instCoeLevel : Coe Level MessageData

Equations

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

instance Lean.MessageData.instCoeExpr : Coe Expr MessageData

Equations

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

instance Lean.MessageData.instCoeName : Coe Name MessageData

Equations

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

instance Lean.MessageData.instCoeSyntax : Coe Syntax MessageData

Equations

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

instance Lean.MessageData.instCoeMVarId : Coe MVarId MessageData

Equations

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

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

Equations

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

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

instance Lean.MessageData.instCoeArrayExpr : Coe (Array Expr) 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 : MessageData) (r : String) : 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 : MessageData) : MessageData

Wrap the given message in parentheses ().

Equations

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

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

Wrap the given message in square brackets [].

Equations

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

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

Append the given list of messages with the given separator.

Equations

• Lean.MessageData.joinSep [] x✝ = Lean.MessageData.ofFormat Std.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 MessageData → 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 ∘ Std.format) "[]"
• Lean.MessageData.ofList x✝ = (Lean.MessageData.joinSep x✝ (Lean.MessageData.ofFormat (Std.Format.text ",") ++ Lean.MessageData.ofFormat Std.Format.line)).sbracket

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

See MessageData.ofList.

Equations

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

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

Puts MessageData into a comma-separated list with "or" at the back (with the serial comma).

Best used on non-empty lists; returns "– none –" for an empty list.

Equations

• Lean.MessageData.orList [] = (Lean.MessageData.ofFormat ∘ Std.format) "– none –"
• Lean.MessageData.orList [x] = x
• Lean.MessageData.orList [x₀, x₁] = x₀ ++ (Lean.MessageData.ofFormat ∘ Std.format) " or " ++ x₁
• Lean.MessageData.orList xs = Lean.MessageData.joinSep xs.dropLast ((Lean.MessageData.ofFormat ∘ Std.format) ", ") ++ (Lean.MessageData.ofFormat ∘ Std.format) ", or " ++ xs.getLast!

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

Puts MessageData into a comma-separated list with "and" at the back (with the serial comma).

Best used on non-empty lists; returns "– none –" for an empty list.

Equations

• Lean.MessageData.andList [] = (Lean.MessageData.ofFormat ∘ Std.format) "– none –"
• Lean.MessageData.andList [x] = x
• Lean.MessageData.andList [x₀, x₁] = x₀ ++ (Lean.MessageData.ofFormat ∘ Std.format) " and " ++ x₁
• Lean.MessageData.andList xs = Lean.MessageData.joinSep xs.dropLast ((Lean.MessageData.ofFormat ∘ Std.format) ", ") ++ (Lean.MessageData.ofFormat ∘ Std.format) ", and " ++ xs.getLast!

def Lean.MessageData.note (note : MessageData) : MessageData

Produces a labeled note that can be appended to an error message.

Equations

• note.note = Lean.MessageData.ofFormat Std.Format.line ++ Lean.MessageData.ofFormat Std.Format.line ++ (Lean.MessageData.ofFormat ∘ Std.format) "Note: " ++ note

def Lean.MessageData.hint' (hint : MessageData) : MessageData

Produces a labeled hint without an associated code action (non-monadic variant of MessageData.hint).

Equations

• hint.hint' = Lean.MessageData.ofFormat Std.Format.line ++ Lean.MessageData.ofFormat Std.Format.line ++ (Lean.MessageData.ofFormat ∘ Std.format) "Hint: " ++ hint

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

Equations

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

instance Lean.MessageData.instCoeListExpr : Coe (List Expr) 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 : Position
• endPos : Option Position
• keepFullRange : Bool

  If true, report range as given; see msgToInteractiveDiagnostic.

• severity : MessageSeverity
• isSilent : Bool

  If true, filter this message from non-language server output. In the language server, silent messages are served as silent diagnostics. See also DiagnosticWith.isSilent?.

• caption : String
• data : α

  The content of the message.

Instances For

• Lean.instFromJsonBaseMessage
• Lean.instInhabitedBaseMessage
• Lean.instToJsonBaseMessage

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

Equations

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

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

Equations

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

instance Lean.instFromJsonBaseMessage {α✝ : Type} [FromJson α✝] : FromJson (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

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 : Position
• endPos : Option Position
• keepFullRange : Bool
• severity : MessageSeverity
• isSilent : Bool
• caption : String
• data : String
• kind : Name

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

Instances For

• Lean.SerialMessage.instToString
• Lean.instFromJsonSerialMessage
• Lean.instToJsonSerialMessage

instance Lean.instToJsonSerialMessage : ToJson SerialMessage

Equations

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

instance Lean.instFromJsonSerialMessage : FromJson SerialMessage

Equations

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

def Lean.errorNameSuffix : String

A suffix added to diagnostic name-containing tags to indicate that they should be used as an error code.

Equations

• Lean.errorNameSuffix = "_namedError"

def Lean.MessageData.tagWithErrorName (msg : MessageData) (name : Name) : MessageData

Produces a MessageData tagged with an identifier for error name.

Note: this function generally should not be called directly; instead, use the macros logNamedError and throwNamedError.

Equations

• msg.tagWithErrorName name = Lean.MessageData.tagged (name.str Lean.errorNameSuffix) msg

def Lean.errorNameOfKind? : Name → Option Name

If the provided name is labeled as a diagnostic name, removes the label and returns the corresponding diagnostic name.

Note: we use this labeling mechanism so that we can have error kinds that are not intended to be shown to the user, without having to validate the presence of an error explanation at runtime.

Equations

• Lean.errorNameOfKind? (p.str last) = if (last == Lean.errorNameSuffix) = true then some p else none
• Lean.errorNameOfKind? x✝ = none

def Lean.MessageData.errorName? (msg : MessageData) : Option Name

Returns the error name with which msg is tagged, if one exists.

Note that this is distinct from msg.kind: the kind of a named-error message is not equal to its name, and there exist message kinds that are not error-name kinds.

Equations

• msg.errorName? = Lean.errorNameOfKind? msg.kind

def Lean.Message.errorName? (msg : Message) : Option Name

Returns the error name with which msg is tagged, if one exists.

Note that this is distinct from msg.kind: the kind of a named-error message is not equal to its name, and there exist message kinds that are not error-name kinds.

Equations

• msg.errorName? = msg.data.errorName?

@[inline]

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

Equations

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

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

Equations

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

instance Lean.SerialMessage.instToString : ToString SerialMessage

Equations

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

@[reducible, inline]

abbrev Lean.Message.kind (msg : Message) : 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

def Lean.Message.isTrace (msg : Message) : Bool

Equations

• msg.isTrace = msg.data.isTrace

@[inline]

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

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

Equations

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

def Lean.Message.toString (msg : Message) (includeEndPos : Bool := false) : BaseIO String

Equations

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

def Lean.Message.toJson (msg : Message) : BaseIO 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 move its messages to reported. Reported messages are preserved for some specific "lookback" operations such as hasError that should consider the entire message history of the current command; most other functions such as add and toList will only operate on unreported messages.

• reported : PersistentArray Message

  The list of messages already reported (i.e. saved in a Snapshot), in insertion order.

• unreported : PersistentArray Message

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

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

Instances For

• Lean.MessageLog.instAppend
• Lean.instInhabitedMessageLog

instance Lean.instInhabitedMessageLog : Inhabited MessageLog

Equations

• Lean.instInhabitedMessageLog = { default := { reported := default, unreported := default, loggedKinds := default } }

def Lean.MessageLog.empty : MessageLog

Equations

• Lean.MessageLog.empty = { }

@[deprecated "renamed to `unreported`; direct access should in general be avoided in favor of using `MessageLog.toList/toArray`" (since := "2024-05-22")]

def Lean.MessageLog.msgs : MessageLog → PersistentArray Message

Equations

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

def Lean.MessageLog.reportedPlusUnreported : MessageLog → PersistentArray Message

Equations

• { reported := r, unreported := u, loggedKinds := loggedKinds }.reportedPlusUnreported = r ++ u

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

Equations

• log.hasUnreported = !log.unreported.isEmpty

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

Equations

• Lean.MessageLog.add msg log = { reported := log.reported, unreported := log.unreported.push msg, loggedKinds := log.loggedKinds }

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

Equations

• l₁.append l₂ = { reported := l₁.reported ++ l₂.reported, unreported := l₁.unreported ++ l₂.unreported, loggedKinds := Lean.RBTree.union l₁.loggedKinds l₂.loggedKinds }

instance Lean.MessageLog.instAppend : Append MessageLog

Equations

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

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

Checks if either of reported or unreported contains an error, i.e. whether the current command has errored yet.

Equations

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

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

Moves unreported messages to reported.

Equations

• log.markAllReported = { reported := log.reported ++ log.unreported, loggedKinds := log.loggedKinds }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

• log.toList = log.unreported.toList

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

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

Equations

• log.toArray = log.unreported.toArray

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

Equations

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

def Lean.indentD (msg : MessageData) : MessageData

Equations

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

def Lean.indentExpr (e : Expr) : MessageData

Equations

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

def Lean.inlineExpr (e : Expr) (maxInlineLength : Nat := 30) : MessageData

Renders an expression e inline in a message unless it will exceed maxInlineLength characters, in which case the expression is indented on a new line.

Note that the output of this function is formatted with preceding and trailing space included. Thus, in m₁ ++ inlineExpr e ++ m₂, m₁ should not end with a space or new line, nor should m₂ begin with one.

Equations

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

def Lean.inlineExprTrailing (e : Expr) (maxInlineLength : Nat := 30) : MessageData

See Lean.inlineExpr. This variation is to be used when the expression is the trailing element of a message; it does not append a newline or space after the expression.

Equations

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

def Lean.aquote (msg : MessageData) : MessageData

Atom quotes

Equations

• Lean.aquote msg = (Lean.MessageData.ofFormat ∘ Std.format) "「" ++ msg ++ (Lean.MessageData.ofFormat ∘ Std.format) "」"

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

• addMessageContext : MessageData → m 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).

Instances

• Lean.Compiler.LCNF.instAddMessageContextCompilerM
• Lean.Core.instAddMessageContextCoreM
• Lean.Elab.Command.instAddMessageContextCommandElabM
• Lean.Elab.Level.instAddMessageContextLevelElabM
• Lean.Meta.instAddMessageContextMetaM
• Lean.instAddMessageContextOfMonadLift

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

Equations

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

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

Equations

• Lean.addMessageContextPartial msgData = do let env ← Lean.getEnv let opts ← Lean.getOptions pure (Lean.MessageData.withContext { env := env, mctx := { }, lctx := { }, opts := opts } msgData)

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

Equations

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

class Lean.ToMessageData (α : Type) : Type

• toMessageData : α → MessageData

Instances

• Aesop.ClusterState.instToMessageData
• Aesop.ElabRuleTerm.instToMessageData
• Aesop.ForwardRuleMatch.instToMessageData
• Aesop.ForwardState.instToMessageData
• Aesop.IndexMatchLocation.instToMessageData
• Aesop.IndexMatchResult.instToMessageData
• Aesop.InstMap.instToMessageData
• Aesop.Match.instToMessageData
• Aesop.Script.Step.instToMessageData
• Aesop.Script.Tactic.instToMessageData
• Aesop.Script.instToMessageDataStepTree
• Aesop.Substitution.instToMessageData
• Aesop.UnorderedArraySet.instToMessageData
• Aesop.VariableMap.instToMessageData
• Aesop.instToMessageDataPINF
• Aesop.instToMessageDataPINFRaw
• Aesop.instToMessageDataRuleState
• Aesop.instToMessageDataRuleTerm
• Lean.Compiler.LCNF.instToMessageDataSpecParamInfo
• Lean.Elab.Structural.instToMessageDataIndGroupInst
• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Op.instToMessageData
• Lean.Elab.Tactic.Do.SpecAttr.instToMessageDataSpecProof
• Lean.Elab.Tactic.RCases.RCasesPatt.instToMessageData
• Lean.Elab.Term.StructInst.instToMessageDataExpandedField
• Lean.Elab.Term.StructInst.instToMessageDataExpandedFieldVal
• Lean.Elab.Term.instToMessageDataArg
• Lean.Meta.Grind.Arith.Offset.instToMessageDataCnstrExpr
• Lean.Meta.Grind.Arith.Offset.instToMessageDataCnstrNodeId
• Lean.Meta.Hint.instToMessageDataSuggestion
• Lean.Meta.Tactic.TryThis.instToMessageDataSuggestion
• Lean.Meta.Tactic.TryThis.instToMessageDataSuggestionText
• Lean.instToMessageDataArray
• Lean.instToMessageDataExpr
• Lean.instToMessageDataFormat
• Lean.instToMessageDataLevel
• Lean.instToMessageDataList
• Lean.instToMessageDataMVarId
• Lean.instToMessageDataMessageData
• Lean.instToMessageDataName
• Lean.instToMessageDataOfToFormat
• Lean.instToMessageDataOption
• Lean.instToMessageDataOptionExpr
• Lean.instToMessageDataProd
• Lean.instToMessageDataString
• Lean.instToMessageDataSubarray
• Lean.instToMessageDataSyntax
• Lean.instToMessageDataTSyntax
• Mathlib.Meta.NormNum.instToMessageDataResult
• Qq.instToMessageDataQuoted
• Simps.instToMessageDataParsedProjectionData
• Simps.instToMessageDataProjectionData
• Simps.instToMessageDataProjectionRule

def Lean.stringToMessageData (str : String) : MessageData

Equations

• Lean.stringToMessageData str = Lean.MessageData.joinSep (List.map (Lean.MessageData.ofFormat ∘ Std.format) (str.split fun (x : Char) => x == '\n')) (Lean.MessageData.ofFormat Std.Format.line)

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

Equations

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

instance Lean.instToMessageDataExpr : ToMessageData Expr

Equations

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

instance Lean.instToMessageDataLevel : ToMessageData Level

Equations

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

instance Lean.instToMessageDataName : ToMessageData Name

Equations

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

instance Lean.instToMessageDataString : ToMessageData String

Equations

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

instance Lean.instToMessageDataSyntax : ToMessageData Syntax

Equations

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

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

Equations

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

instance Lean.instToMessageDataFormat : ToMessageData Format

Equations

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

instance Lean.instToMessageDataMVarId : ToMessageData MVarId

Equations

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

@[defaultInstance 1000]

instance Lean.instToMessageDataMessageData : ToMessageData MessageData

Equations

• Lean.instToMessageDataMessageData = { toMessageData := id }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

instance Lean.instToMessageDataOptionExpr : ToMessageData (Option Expr)

Equations

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

def Lean.termM!_ : ParserDescr

Equations

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

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

Equations

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

def Lean.Kernel.Exception.toMessageData (e : Exception) (opts : Options) : MessageData

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Kernel.Exception.other msg).toMessageData opts = Lean.toMessageData "(kernel) " ++ Lean.toMessageData msg ++ Lean.toMessageData ""
• Lean.Kernel.Exception.deterministicTimeout.toMessageData opts = (Lean.MessageData.ofFormat ∘ Std.format) "(kernel) deterministic timeout"
• Lean.Kernel.Exception.excessiveMemory.toMessageData opts = (Lean.MessageData.ofFormat ∘ Std.format) "(kernel) excessive memory consumption detected"
• Lean.Kernel.Exception.deepRecursion.toMessageData opts = (Lean.MessageData.ofFormat ∘ Std.format) "(kernel) deep recursion detected"
• Lean.Kernel.Exception.interrupted.toMessageData opts = (Lean.MessageData.ofFormat ∘ Std.format) "(kernel) interrupted"

def Lean.toTraceElem {α : Type} [ToMessageData α] (e : α) (cls : Name := Name.mkSimple "_") : MessageData

Helper functions for creating a MessageData with the given header and elements.

Equations

• Lean.toTraceElem e cls = Lean.MessageData.trace { cls := cls } (Lean.toMessageData e) #[]