Email Gateway (Nov 29 2024 at 09:30): Email Gateway (Nov 29 2024 at 09:30):From: "\"Putti, Edoardo (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle users,
I'm tutoring students in a master course. One of the learning objectives for this week was finding theorems.
Because of the syntax translations it's hard for them to go from a term such as "{1, 2, 3}" to
"insert 1 (insert 2 (insert 3 bot)))" in their head and therefore actually use find_theorems to get unstuck.
*
Is there an option to "turn off" syntax?
*
Is there a way to get all syntax translations involved in a term parsing/unparsing?
*
Is there a way to go to the syntax rules definition?
Email Gateway (Nov 29 2024 at 14:41):From: i n <cl-isabelle-users@lists.cam.ac.uk>
Hi, Im pretty sure you should be able to use this
no_translations
"{x, xs}" ⇌ "CONST insert x {xs}"
"{x}" ⇌ "CONST insert x {}"
no_syntax
"_Finset" :: "args ⇒ 'a set" ("{(_)}")
Bundles don't support translations so you cant really use bundles. You have to remove the translation before removing the syntax. (This feature should be supported if any isabelle developer sees this)
Also you need to ensure all your theories are based of this and you do not have another theory that imports Main or HOL.* directly without this or you will get the set syntax back due to the import.
Cheers,
Irvin
On Friday, 29 November 2024 at 09:30:42 am UTC, \"Putti, Edoardo (UT-EEMCS)\"" (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk> wrote:
#yiv2145379254 P {margin-top:0;margin-bottom:0;}Dear Isabelle users,
I'm tutoring students in a master course. One of the learning objectives for this week was finding theorems.
Because of the syntax translations it's hard for them to go from a term such as "{1, 2, 3}" to"insert 1 (insert 2 (insert 3 bot)))" in their head and therefore actually use find_theorems to get unstuck.
- Is there an option to "turn off" syntax?
- Is there a way to get all syntax translations involved in a term parsing/unparsing?
- Is there a way to go to the syntax rules definition?
Email Gateway (Dec 01 2024 at 14:47):From: Makarius <makarius@sketis.net>
On 29/11/2024 10:30, "Putti, Edoardo (UT-EEMCS)" (via cl-isabelle-users
Mailing List) wrote:
I'm tutoring students in a master course. One of the learning objectives for
this week was finding theorems.Because of the syntax translations it's hard for them to go from a term such
as "{1, 2, 3}" to
"insert 1 (insert 2 (insert 3 bot)))" in their head and therefore actually use
find_theorems to get unstuck.
Note that Isabelle2025 (March 2025) will have a lot of extra markup, both in
the input and output of the term language. Thus you can hover over the curly
braces above to get to the underlying constant "Set.insert". Moreover,
inner-syntax blocks will be highlighted, together with semi-formal comments
about their purpose: above that is 'notation: mixfix "set enumeration"' --- it
is up to the library to defined that for mixfix, while infix and binder are
automatic.
You can try it e.g. with current Isabelle/e8b388c2b490 or a snapshot from
https://isatest.sketis.net/devel/release_snapshot
Note that the release schedule is here
https://isabelle-dev.sketis.net/phame/post/view/77/plan_for_isabelle2025_release
* Is there an option to "turn off" syntax?
You can approximate that in Isabelle/ML as follows, but the result contains a
lot of extra details:
ML ‹@{term ‹{1, 2, 3}›}›
* Is there a way to get all syntax translations involved in a term parsing/
unparsing?
See the command 'print_syntax', but the result contains a lot of extra details.
* Is there a way to go to the syntax rules definition?
There is no direct way for that, only indirectly because the formal link e.g.
to constant "Set.insert" gets you where the translations are also defined.
(The reason for the lack of links for 'syntax' and 'translations' is that
these have no formal status; there is just one big bucket of unscoped/untyped
things.)
Instead of showing too much low-level things, I would rather teach beginners
to work with PIDE markup, both in the input buffer or output panel.
Makarius
Last updated: Jan 04 2025 at 20:18 UTC