Email Gateway (Oct 31 2025 at 12:03): Email Gateway (Oct 31 2025 at 12:03):From: "\"Putti, Edoardo (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
Hello all,
I'm surely working against the pretty-printing and syntax but what I found in Pure/HOL/AFP does not seems to address this issue I am facing.
I want to print a type in prefix notation, e.g. option 'a, in place of postfix notation, 'a option.
After spelunking in pure_theory.ML I got to the syntax definition for type application and I can override the normal syntax with mine for a custom print mode.
syntax (pvl output)
"_tapp" :: "type => type_name => type" ("(1_<_>)")
typ "'a option" (* prints as 'a option *)
typ (pvl) "'a option" (* prints as 'a<option> *)
I cannot exchange the order of in the mixfix declaration but I can declare a new pattern _pvl_tapp and a translation from _tapp to _pvl_tapp.
syntax (pvl output)
"_pvl_tapp" :: " type_name => type => type" ("(1_<_>)") (* note inversion of type_name and type in production *)
typ "'a option" (* prints as 'a option *)
typ (pvl) "'a option" (* prints as 'a option, expected as I have no translation yet *)
translation
"_pvl_tapp tc ty" == "_tapp ty tc"
typ "'a option" (* prints as 'a option *)
typ (pvl) "'a option" (* prints as 'a option *)
I even got as far as looking at type_syntax but that binds one syntax constant to one type or type synonym. I would need to
do this binding for each type which is unsatisfactory.
Decorating the translation with the (type) qualifier (?) yields the error Undefined type name: "_pvl_tapp", example below.
translation
(type) "_pvl_tapp tc ty" == (type) "_tapp ty tc"
Is this use-case supported in any way? It's also unclear how to interface with the type pretty printing and I cannot find anybody attempting this.
The second question is, it there a way to scope translations to one printing mode? In the previous example the translation from _tapp to _pvl_tapp makes no
sense in normal output so it should be ignored by the system, which is what I am observing now.
I'm attaching a theory file where you can reproduce this behavior.
Last updated: Nov 09 2025 at 20:21 UTC