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

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

Equations

• Lean.instTypeNameMessageData = Lean.inst✝

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 : optParam (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 : Lake.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 subtress (.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.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.

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.

instance Lean.instInhabitedMessageLog : Inhabited Lean.MessageLog

Equations

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

def Lean.MessageLog.empty : Lean.MessageLog

Equations

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

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

Equations

• log.hasUnreported = !log.unreported.isEmpty

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 }

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

Equations

• l₁.append l₂ = { hadErrors := l₁.hadErrors || l₂.hadErrors, unreported := l₁.unreported ++ l₂.unreported }

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.hadErrors || log.unreported.any fun (x : Lean.Message) => match x.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

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

Equations

• log.toList = log.unreported.toList

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

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

Equations

• log.toArray = log.unreported.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

  Without context, a MessageData object may be 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 : 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.