lean4-metaprogramming-book icon indicating copy to clipboard operation
lean4-metaprogramming-book copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

metam: add section on debugging

Open JLimperg opened this issue 1 year ago • 1 comments

Just leaving this here as a note to myself (or to anyone else who wants to do this of course). I think this would be very helpful. I'm thinking of covering ppExpr, the elab trick, dbg_trace, trace[debug], probably other stuff.

JLimperg avatar Jul 21 '22 15:07 JLimperg

Just dropping this link from the Lean4 manual for the record.

ydewit avatar Sep 03 '22 16:09 ydewit