Email Gateway (Apr 20 2021 at 09:31): Email Gateway (Apr 20 2021 at 09:31):From: Manuel Eberl <eberlm@in.tum.de>
Hello,
abbreviations can sometimes make terms a bit intransparent if you don't
know what they mean, e.g.
"∀⇩F n in sequentially. ln (real n) > 0"
is internally
"eventually (λn. 0 < ln (real n)) sequentially"
but this is not so easy to find out. You cannot even ctrl+click on
anything due to the custom syntax.
So, is there an easy way to print a term
without any abbreviations, but with notation (e.g. I don't want to
see "plus x y" instead of "x + y")
without abbreviations and without notation (i.e. "plus x y" instead
of "x + y")
The closest thing I am aware of is to do something like
ML_val ‹@{term "∀⇩F n in sequentially. n > 0"}›
Manuel
smime.p7s
Email Gateway (Apr 20 2021 at 10:59):From: Dominique Unruh <unruh@ut.ee>
You could try
ML_val ‹
Syntax.string_of_term_global \<^theory>‹Main› \<^term>‹∀⇩F n in
sequentially. n > 0› |> writeln
›
It's not optimal, but probably more readable that your approach. And you
can replace Main by other theories to fine-tune the amount of syntax.
(E.g., Pure for no syntactic sugar.) Main drawback are annoying question
marks in the latter case.
Best wishes,
Dominique.
Email Gateway (Apr 20 2021 at 11:04):From: Manuel Eberl <eberlm@in.tum.de>
I think we should really strive for something more nice-to-use and
"official". Two more people have written to me privately that they would
really want to have something like this.
Manuel
Email Gateway (Apr 20 2021 at 11:11):From: Peter Lammich <lammich@in.tum.de>
I'm also using an "inofficial" hack if the term structure is not clear
to me, and would like to see something that works better and reliably.
Email Gateway (Jul 07 2021 at 14:13):From: Mikhail Mandrykin <mandrykin@ispras.ru>
I recently tackled with similar situations and for now implemented a
workaround/hack that works quite acceptably for me. It declares a
configuration option "bypass_translations" similar to "show_abbrevs",
and the option, when enabled, prevents print_translations and
print_ast_translations from being applied by temporarily prefixing all
constant names with a relatively uncommon symbol (e.g. '@'). Meanwhile,
it leaves alone the constants that have the type "prop" as their
argument or result types. This option is relatively convenient as it
works well for goal statements, retains trivial infix notations (but not
binders and more complex stuff) and notations from the Pure kernel (e.g.
‹⟦…⟧›). Usually it's enough to add ‹using [[show_abbrevs=false,
bypass_translations=true]]› to enable it temporarily for the current
goal. Attached the theory and a sample goal snapshot
Regards,
Mikhail
Peter Lammich писал 2021-04-20 14:11:
Bypass_Translations.thy
goal_untranslated.png
goal_translated.png
Last updated: Jan 04 2025 at 20:18 UTC