Email Gateway (Aug 19 2022 at 12:42): Email Gateway (Aug 19 2022 at 12:42):From: Peter Lammich <lammich@in.tum.de>
Hi all.
Consider the following:
imports Complex_Main
begin
term "∃a::nat. ∃b::nat. ∃c::real. a+b+c=0"
The output is:
"∃x xa c. real x + real xa + c = 0"
:: "bool"
Thus, instead of my original variable names, I get synthetic names
x,xa, ..., which makes the term less readable.
Is there any special reason why the variables have to be renamed?
Otherwise, it would be nice to keep the original names.
Email Gateway (Aug 19 2022 at 12:42):From: Dmitriy Traytel <traytel@in.tum.de>
It is the same reason as in the other theread on coercions
(https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-November/msg00243.html):
mapping over functions in conjunction with beta reduction.
Dmitriy
Last updated: Apr 25 2024 at 12:23 UTC