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✝ }

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.

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: Lake.Name → Lean.MessageData → Array Lean.MessageData → Bool → Lean.MessageData

instance Lean.instInhabitedMessageData : Inhabited Lean.MessageData

Equations

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

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

Determines whether the message contains any content.

Equations

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

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

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

def Lean.MessageData.nil : Lean.MessageData

An empty message.

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

• Lean.MessageData.ofLevel l = Lean.MessageData.ofFormat (Std.format l)

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

• Lean.MessageData.hasSyntheticSorry msg = 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

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

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

Equations

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

instance Lean.MessageData.instAppendMessageData : Append Lean.MessageData

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

instance Lean.MessageData.instCoeOptionExprMessageData : 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.instCoeArrayExprMessageData : Coe (Array Lean.Expr) Lean.MessageData

Equations

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

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

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

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

Wrap the given message in parentheses ().

Equations

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

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

Wrap the given message in square brackets [].

Equations

• Lean.MessageData.sbracket f = 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 (Array.toList msgs)

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

Equations

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

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

Equations

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

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

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

  The content of the message.

instance Lean.instInhabitedMessage : Inhabited Lean.Message

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

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

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

• Lean.MessageLog.isEmpty log = Lean.PersistentArray.isEmpty log.msgs

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

Equations

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

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

Equations

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

instance Lean.MessageLog.instAppendMessageLog : Append Lean.MessageLog

Equations

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

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

Equations

• Lean.MessageLog.hasErrors log = Lean.PersistentArray.any log.msgs 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

• 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

• Lean.MessageLog.forM log f = Lean.PersistentArray.forM log.msgs f

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

Equations

• Lean.MessageLog.toList log = List.reverse (Lean.PersistentArray.foldl log.msgs (fun (acc : List Lean.Message) (msg : Lean.Message) => msg :: acc) [])

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

Equations

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

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

Equations

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

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.instAddMessageContext (m : Type → Type) (n : Type → Type) [MonadLift m n] [Lean.AddMessageContext m] : Lean.AddMessageContext n

Equations

• Lean.instAddMessageContext 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.instToMessageData {α : Type} [Lean.ToFormat α] : Lean.ToMessageData α

Equations

• Lean.instToMessageData = { 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 (Array.toList as) }

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

Equations

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

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 (Array.toList msgs) (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.