source
def Lake.mkParserErrorMessage (ictx : Lean.Parser.InputContext) (s : Lean.Parser.ParserState) (e : Lean.Parser.Error) :
Lean.Message
Equations

- Lake.mkParserErrorMessage ictx s e = { fileName := ictx.fileName, pos := ictx.fileMap.toPosition s.pos, keepFullRange := true, data := (Lean.MessageData.ofFormat ∘ Std.format) (toString e) }

Instances For

source
def Lake.mkExceptionMessage (ictx : Lean.Parser.InputContext) (e : Lean.Exception) :
Lean.Message
Equations

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

Instances For

source
def Lake.mkMessageNoPos (ictx : Lean.Parser.InputContext) (data : Lean.MessageData) (severity : Lean.MessageSeverity := Lean.MessageSeverity.error) :
Lean.Message
Equations

- Lake.mkMessageNoPos ictx data severity = { fileName := ictx.fileName, pos := ictx.fileMap.toPosition 0, severity := severity, data := data }

Instances For

source
def Lake.mkMessageStringCore (severity : Lean.MessageSeverity) (fileName caption body : String) (pos : Lean.Position) (endPos? : Option Lean.Position := none) (infoWithPos : Bool := false) :
String
Equations

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

Instances For

source
def Lake.mkMessageString (msg : Lean.Message) (includeEndPos infoWithPos : Bool := false) :
BaseIO String
Equations

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

Instances For

source
def Lake.mkMessageLogString (log : Lean.MessageLog) :
BaseIO String
Equations

- Lake.mkMessageLogString log = List.foldlM (fun (s : String) (m : Lean.Message) => do let __do_lift ← Lake.mkMessageString m false true pure (s ++ __do_lift)) "" log.toList

Instances For