- getRef : m Lean.Syntax
- getFileName : m String
- hasErrors : m Bool
- logMessage : Lean.Message → m Unit
instance
Lean.instMonadLog
(m : Type → Type)
(n : Type → Type)
[inst : MonadLift m n]
[inst : Lean.MonadLog m]
:
Equations
- Lean.instMonadLog m n = Lean.MonadLog.mk (liftM Lean.MonadLog.getRef) (liftM Lean.getFileName) (liftM Lean.MonadLog.hasErrors) fun msg => liftM (Lean.logMessage msg)
Equations
- Lean.getRefPos = do let ref ← Lean.MonadLog.getRef pure (Option.getD (Lean.Syntax.getPos? ref) 0)
Equations
- Lean.getRefPosition = do let fileMap ← Lean.getFileMap let a ← Lean.getRefPos pure (Lean.FileMap.toPosition fileMap a)
def
Lean.logAt
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadLog m]
[inst : Lean.AddMessageContext m]
(ref : Lean.Syntax)
(msgData : Lean.MessageData)
(severity : optParam Lean.MessageSeverity Lean.MessageSeverity.error)
:
m Unit
Equations
- One or more equations did not get rendered due to their size.
def
Lean.logErrorAt
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadLog m]
[inst : Lean.AddMessageContext m]
(ref : Lean.Syntax)
(msgData : Lean.MessageData)
:
m Unit
Equations
- Lean.logErrorAt ref msgData = Lean.logAt ref msgData
def
Lean.logWarningAt
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadLog m]
[inst : Lean.AddMessageContext m]
(ref : Lean.Syntax)
(msgData : Lean.MessageData)
:
m Unit
Equations
- Lean.logWarningAt ref msgData = Lean.logAt ref msgData Lean.MessageSeverity.warning
def
Lean.logInfoAt
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadLog m]
[inst : Lean.AddMessageContext m]
(ref : Lean.Syntax)
(msgData : Lean.MessageData)
:
m Unit
Equations
- Lean.logInfoAt ref msgData = Lean.logAt ref msgData Lean.MessageSeverity.information
def
Lean.log
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadLog m]
[inst : Lean.AddMessageContext m]
(msgData : Lean.MessageData)
(severity : optParam Lean.MessageSeverity Lean.MessageSeverity.error)
:
m Unit
Equations
- Lean.log msgData severity = do let ref ← Lean.MonadLog.getRef Lean.logAt ref msgData severity
def
Lean.logError
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadLog m]
[inst : Lean.AddMessageContext m]
(msgData : Lean.MessageData)
:
m Unit
Equations
- Lean.logError msgData = Lean.log msgData
def
Lean.logWarning
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadLog m]
[inst : Lean.AddMessageContext m]
(msgData : Lean.MessageData)
:
m Unit
Equations
- Lean.logWarning msgData = Lean.log msgData Lean.MessageSeverity.warning
def
Lean.logInfo
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadLog m]
[inst : Lean.AddMessageContext m]
(msgData : Lean.MessageData)
:
m Unit
Equations
- Lean.logInfo msgData = Lean.log msgData Lean.MessageSeverity.information
def
Lean.logTrace
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadLog m]
[inst : Lean.AddMessageContext m]
(cls : Lean.Name)
(msgData : Lean.MessageData)
:
m Unit
Equations
- One or more equations did not get rendered due to their size.
def
Lean.logUnknownDecl
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadLog m]
[inst : Lean.AddMessageContext m]
(declName : Lean.Name)
:
m Unit
Equations
- Lean.logUnknownDecl declName = Lean.logError (Lean.toMessageData "unknown declaration '" ++ Lean.toMessageData declName ++ Lean.toMessageData "'")