Re: [isabelle] Coercions rename bound variables

Am 26.11.2013 13:39, schrieb Peter Lammich:
Hi all.

Consider the following:

imports Complex_Main

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.


It is the same reason as in the other theread on coercions ( mapping over functions in conjunction with beta reduction.


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