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

Equations

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

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 : optParam Lean.MessageSeverity Lean.MessageSeverity.error) : Lean.Message

Equations

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

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

Equations

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

def Lake.mkMessageString (msg : Lean.Message) (includeEndPos : optParam Bool false) (infoWithPos : optParam 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