Re: [isabelle] Coercions rename bound variables



Am 26.11.2013 13:39, schrieb Peter Lammich:
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.

--
   Peter

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




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