Email Gateway (Apr 27 2023 at 01:48): Email Gateway (Apr 27 2023 at 01:48):From: Peter Gammie <peteg42@gmail.com>
Hello,
I just tried to use \<bbbA> (βπΈβ) as a variable. (It appears in the Symbols panel β can we also have a non-bold variant?) The lexer chokes on it.
term "\<bbbA>"
Inner lexical errorβ
Failed to parse term
Also what does the trailing βββ in the above error signify?
cheers,
peter
Email Gateway (Apr 27 2023 at 09:23):From: Makarius <makarius@sketis.net>
On 27/04/2023 03:44, Peter Gammie wrote:
I just tried to use \<bbbA> (βπΈβ) as a variable. (It appears in the Symbols panel β can we also have a non-bold variant?) The lexer chokes on it.
\<bbbA> is not a letter. You need to use it with 'notation' or 'write' in a
proof.
See also the isar-ref manual on the syntax category "letter".
Also what does the trailing βββ in the above error signify?
CTRL-hover-click in the Prover IDE will tell you: It is a formal position.
Makarius
Last updated: Jan 04 2025 at 20:18 UTC