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

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.

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 }

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.

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.

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