Re: [isabelle] changing the printed syntax for "Some x" (was Re: syntax for a type abbreviations)



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.