Documentation

Lake.Util.Message

def Lake.mkMessageStringCore (severity : Lean.MessageSeverity) (fileName caption body : String) (pos : Lean.Position) (endPos? : Option Lean.Position := none) (infoWithPos : Bool := false) :
Equations
    Instances For
      def Lake.mkMessageString (msg : Lean.Message) (includeEndPos infoWithPos : Bool := false) :
      Equations
        Instances For
          Equations
            Instances For