max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add MessageData.nestD

Browse source 
"default nest"
This commit is contained in:
Leonardo de Moura 2020-08-27 11:22:47 -07:00
parent 99161538f8
commit 5349a73655
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Message.lean
View file

@ -180,8 +180,11 @@ def toList (log : MessageLog) : List Message :=
end MessageLog
def MessageData.nestD (msg : MessageData) : MessageData :=
MessageData.nest 2 msg
def indentExpr (msg : MessageData) : MessageData :=
MessageData.nest 2 (Format.line ++ msg)
MessageData.nestD (Format.line ++ msg)
namespace KernelException