You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In this screenshot, the highlighting of dbgTraceIfShared is a bit funky:
It seems to me that the issue comes from here, where there is no word-end in the rx call, and that dbgTraceIfShared should be part of lean4-debugging as well.
Would a PR be welcome with this change?
Also, why do they call eval? It seems to me that eval on top of quote should just be ordinary code. Could that be removed in the same PR?
The text was updated successfully, but these errors were encountered:
In this screenshot, the highlighting of
dbgTraceIfShared
is a bit funky:It seems to me that the issue comes from here, where there is no
word-end
in therx
call, and thatdbgTraceIfShared
should be part oflean4-debugging
as well.Would a PR be welcome with this change?
Also, why do they call
eval
? It seems to me thateval
on top ofquote
should just be ordinary code. Could that be removed in the same PR?The text was updated successfully, but these errors were encountered: