Open JLimperg opened 2 years ago
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.
ppExpr
elab
dbg_trace
trace[debug]
Just dropping this link from the Lean4 manual for the record.
ydewit
commented
2 years ago
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, theelabtrick,dbg_trace,trace[debug], probably other stuff.