Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] \<bbbA>


view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 20:16 UTC