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

chore: remove workaround

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-10 07:47:28 -07:00
parent 2bc25935c6
commit 446b7dc690
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

@ -137,7 +137,7 @@ macro:max "trace!" id:term:max msg:term : term => `(trace $id fun _ => ($msg : M
syntax[traceInterp] "trace[" ident "]!" term : term
macro_rules[Lean.traceInterp] -- Fix kind resolution
macro_rules[traceInterp]
| `(trace[$id]! $s) => `(Lean.trace $(quote id.getId) fun _ => ($s : MessageData))
end Lean