Email Gateway (Aug 22 2022 at 14:15): Email Gateway (Aug 22 2022 at 14:15):From: Lars Hupel <hupel@in.tum.de>
Dear Makarius,
it seems that in some situations, the "error" markup covers a too large
region. Here's a small example:
lemma True
proof -
have False
sorry
―‹abc›
The comment is also highlighted in red.
Cheers
Lars
Last updated: Nov 21 2024 at 12:39 UTC