Email Gateway (Aug 18 2022 at 12:38): Email Gateway (Aug 18 2022 at 12:38):From: Patrice Chalin <chalin@encs.concordia.ca>
On a related note: how can I get "Some x" to display as, say, "[x]"?
Thanks
Patrice Chalin wrote:
Email Gateway (Aug 18 2022 at 12:38):From: Makarius <makarius@sketis.net>
On Mon, 17 Nov 2008, Patrice Chalin wrote:
On a related note: how can I get "Some x" to display as, say, "[x]"?
This can be done in a simple and robust way by using the modern
specification element 'notation' --- which works for term syntax (consts
or local fixes):
notation Some ("(\<lfloor>_\<rfloor>)")
I have the following type abbreviations:
types
ValOrUndef = "Val option"
"Val\<^isub>\<bottom>" = ValOrUndef(the above actually parses fine). But then I cannot use
Val\<^isub>\<bottom> in places where a type is expected because a syntax
error is reported. Is there any way I can get ValOrUndef to be printed (in
PDF versions of the theory) as Val\<^isub>\<bottom>?
In the above 'types' declaration, the outer syntax name
"Val\<^isub>\<bottom>" is not a valid identifier. Since 'types' belongs
to an ancient layer of logical primitives, there is no extra check here.
The error is only seen much later when trying to input such types as inner
syntax.
You need to use concrete syntax as mixfix annotation, but there is nothing
like 'type_notation' at the moment. Using the low-level 'syntax'
primitive instead, we can associate certain mixfix grammar clauses
directly with the syntactic constant "option" (which is still the way type
constructors are represented in the syntax tree, until we make type syntax
``authentic'' -- this is another story).
So it works at the moment like this:
syntax
option :: "type => type" ("_\<^sub>\<bottom>" [1000] 1000)
Here are some examples:
term "Some x"
term "Some (Some x)"
term "Some (Some [x])"
As usual with the current version of the Isabelle document preparation
system, you only get the alternative notation if you write the sources
with that syntax in the first place, or if you print inner logical
entities explicitly, e.g. via @{term} or @{thm} antiquotations.
Makarius
Last updated: May 03 2024 at 08:18 UTC