# Documentation

Lean.Message

def Lean.mkErrorStringWithPos (fileName : String) (pos : Lean.Position) (msg : String) (endPos : optParam () none) :
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations

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

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

Instances For
structure Lean.PPFormat :
• Pretty-prints text using surrounding context, if any.

• Searches for synthetic sorries in original input. Used to filter out certain messages.

hasSyntheticSorry :

Lazily formatted text to be used in MessageData.

Instances For
• Eagerly formatted text. We inspect this in various hacks, so it is not immediately subsumed by ofPPFormat.

ofFormat:
• Lazily formatted text.

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

withContext:
• withNamingContext:
• Lifted Format.nest

nest:
• Lifted Format.group

group:
• Lifted Format.compose

compose:
• 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".

tagged:
• trace:

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

Instances For

Determines whether the message contains any content.

Equations
partial def Lean.MessageData.hasTag (p : ) :

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

An empty message.

Equations
Equations
• Lean.MessageData.mkPPContext nCtx ctx = { env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts, currNamespace := nCtx.currNamespace, openDecls := nCtx.openDecls }
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.

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.

Wrap the given message in parentheses ().

Equations

Wrap the given message in square brackets [].

Equations

Append the given list of messages with the given separarator.

Equations

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.

See MessageData.ofList.

Equations
Equations
structure Lean.Message :

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.

Instances For
Equations
• Lean.instInhabitedMessage = { default := { fileName := default, pos := default, endPos := default, severity := default, caption := default, data := default } }
def Lean.Message.toString (msg : Lean.Message) (includeEndPos : ) :
Equations
• One or more equations did not get rendered due to their size.

A persistent array of messages.

Instances For
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• = { msgs := l₁.msgs ++ l₂.msgs }
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.MessageLog.forM {m : } [inst : ] (log : Lean.MessageLog) (f : ) :
Equations
Equations
Equations
Instances
instance Lean.instAddMessageContext (m : ) (n : ) [inst : ] [inst : ] :
Equations
• = { addMessageContext := fun msg => }
def Lean.addMessageContextPartial {m : } [inst : ] [inst : ] [inst : ] (msgData : Lean.MessageData) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.addMessageContextFull {m : } [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] (msgData : Lean.MessageData) :
Equations
• One or more equations did not get rendered due to their size.
• toMessageData :
Instances
Equations
• One or more equations did not get rendered due to their size.
instance Lean.instToMessageData {α : Type} [inst : ] :
Equations
Equations
• Lean.instToMessageDataTSyntax = { toMessageData := fun x => }
Equations
instance Lean.instToMessageDataList {α : Type} [inst : ] :
Equations
instance Lean.instToMessageDataArray {α : Type} [inst : ] :
Equations
• Lean.instToMessageDataArray = { toMessageData := fun as => }
instance Lean.instToMessageDataSubarray {α : Type} [inst : ] :
Equations
• Lean.instToMessageDataSubarray = { toMessageData := fun as => }
instance Lean.instToMessageDataOption {α : Type} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.