Documentation

Lean.Message

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

Equations

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

inductive Lean.MessageSeverity:

Type

instance Lean.instInhabitedMessageSeverity:

Inhabited Lean.MessageSeverity

Equations

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

instance Lean.instBEqMessageSeverity:

BEq Lean.MessageSeverity

Equations

Lean.instBEqMessageSeverity = { beq := [anonymous] }

structure Lean.MessageDataContext:

Type

structure Lean.NamingContext:

Type

currNamespace : Lean.Name
openDecls : List Lean.OpenDecl

inductive Lean.MessageData:

Type

ofFormat: Lean.Format → Lean.MessageData
ofSyntax: Lean.Syntax → Lean.MessageData
ofExpr: Lean.Expr → Lean.MessageData
ofLevel: Lean.Level → Lean.MessageData
ofName: Lean.Name → Lean.MessageData
ofGoal: Lean.MVarId → Lean.MessageData
withContext: Lean.MessageDataContext → Lean.MessageData → Lean.MessageData
withNamingContext: Lean.NamingContext → Lean.MessageData → Lean.MessageData
nest: Nat → Lean.MessageData → Lean.MessageData
group: Lean.MessageData → Lean.MessageData
compose: Lean.MessageData → Lean.MessageData → Lean.MessageData
tagged: Lean.Name → Lean.MessageData → Lean.MessageData
node: Array Lean.MessageData → Lean.MessageData

instance Lean.instInhabitedMessageData:

Inhabited Lean.MessageData

Equations

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

partial def Lean.MessageData.isEmpty:

Lean.MessageData → Bool

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

Lean.MessageData

Equations

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

partial def Lean.MessageData.instantiateMVars.visit (msg : Lean.MessageData) (mctx : Lean.MetavarContext) :

Lean.MessageData

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

Lean.MessageData → Bool

def Lean.MessageData.nil:

Lean.MessageData

Equations

Lean.MessageData.nil = Lean.MessageData.ofFormat Lean.Format.nil

def Lean.MessageData.isNil:

Lean.MessageData → Bool

Equations

Lean.MessageData.isNil _fun_discr = match _fun_discr with | Lean.MessageData.ofFormat Lean.Format.nil => true | x => false

def Lean.MessageData.isNest:

Lean.MessageData → Bool

Equations

Lean.MessageData.isNest _fun_discr = match _fun_discr with | Lean.MessageData.nest a a_1 => true | x => false

def Lean.MessageData.mkPPContext (nCtx : Lean.NamingContext) (ctx : Lean.MessageDataContext) :

Equations

Lean.MessageData.mkPPContext nCtx ctx = { env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts, currNamespace := nCtx.currNamespace, openDecls := nCtx.openDecls }

partial def Lean.MessageData.formatAux:

Lean.NamingContext → Option Lean.MessageDataContext → Lean.MessageData → IO Lean.Format

def Lean.MessageData.format (msgData : Lean.MessageData) :

Equations

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

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

Equations

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

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

Lean.MessageData.instCoeArrayExprMessageData = { coe := fun es => Lean.MessageData.arrayExpr.toMessageData es 0 (Function.comp Lean.MessageData.ofFormat Lean.format "#[") }

def Lean.MessageData.bracket (l : String) (f : Lean.MessageData) (r : String) :

Lean.MessageData

Equations

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

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

Lean.MessageData

Equations

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

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

Lean.MessageData

Equations

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

def Lean.MessageData.joinSep:

List Lean.MessageData → Lean.MessageData → Lean.MessageData

Equations

Lean.MessageData.joinSep [] _fun_discr = Lean.MessageData.ofFormat Lean.Format.nil
Lean.MessageData.joinSep [a] _fun_discr = a
Lean.MessageData.joinSep (a :: as) _fun_discr = a ++ _fun_discr ++ Lean.MessageData.joinSep as _fun_discr

def Lean.MessageData.ofList:

List Lean.MessageData → Lean.MessageData

Equations

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

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

Lean.MessageData

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 => Lean.MessageData.ofList (List.map Lean.MessageData.ofExpr es) }

structure Lean.Message:

Type

fileName : String
pos : Lean.Position
endPos : Option Lean.Position
severity : Lean.MessageSeverity
caption : String
data : Lean.MessageData

instance Lean.instInhabitedMessage:

Inhabited Lean.Message

Equations

Lean.instInhabitedMessage = { default := { fileName := default, pos := default, endPos := default, severity := default, caption := default, data := default } }

def Lean.Message.toString (msg : Lean.Message) (includeEndPos : optParam Bool false) :

Equations

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

structure Lean.MessageLog:

Type

msgs : Std.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) :

Equations

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

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

Lean.MessageLog

Equations

Lean.MessageLog.add msg log = { msgs := Std.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) :

Equations

Lean.MessageLog.hasErrors log = Std.PersistentArray.any log.msgs fun m => 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} [inst : Monad m] (log : Lean.MessageLog) (f : Lean.Message → m Unit) :

Equations

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

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

List Lean.Message

Equations

Lean.MessageLog.toList log = List.reverse (Std.PersistentArray.foldl log.msgs (fun acc msg => 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

Instances

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

Lean.AddMessageContext n

Equations

Lean.instAddMessageContext m n = { addMessageContext := fun msg => liftM (Lean.addMessageContext msg) }

def Lean.addMessageContextPartial {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : 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} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadMCtx m] [inst : Lean.MonadLCtx m] [inst : 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

Instances

def Lean.stringToMessageData (str : String) :

Lean.MessageData

Equations

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

instance Lean.instToMessageData {α : Type} [inst : Lean.ToFormat α] :

Lean.ToMessageData α

Equations

Lean.instToMessageData = { toMessageData := Lean.MessageData.ofFormat ∘ Lean.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 Lean.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 a => Lean.MessageData.ofSyntax a.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} [inst : Lean.ToMessageData α] :

Lean.ToMessageData (List α)

Equations

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

instance Lean.instToMessageDataArray {α : Type} [inst : Lean.ToMessageData α] :

Lean.ToMessageData (Array α)

Equations

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

instance Lean.instToMessageDataSubarray {α : Type} [inst : Lean.ToMessageData α] :

Lean.ToMessageData (Subarray α)

Equations

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

instance Lean.instToMessageDataOption {α : Type} [inst : Lean.ToMessageData α] :

Lean.ToMessageData (Option α)

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.