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

chore: restore macro

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-19 19:08:35 -07:00
parent 3348e3c3a1
commit d2ee641e7f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Util/Trace.lean
View file

@ -133,6 +133,6 @@ new_frontend
namespace Lean
-- macro:max "trace!" id:term:max msg:term : term => `(trace $id fun _ => ($msg : MessageData))
macro:max "trace!" id:term:max msg:term : term => `(trace $id fun _ => ($msg : MessageData))
end Lean