Email Gateway (Aug 23 2022 at 09:05): Email Gateway (Aug 23 2022 at 09:05):From: Peter Lammich <lammich@in.tum.de>
Hi List,
I ran into an odd effect: inside an experiment environment,
"definition" sometimes seems to produce (partially) eta-expanded terms
instead of constants! For me, it occurs in one of my own tools, and I
could not yet strip it down, but I found the same strange effect in the
standard "definition" command, when it automatically augments a type
argument. Outside an experiment environment, everything is as expected.
(minimal example attached)
What is going on here? To fix this thing for my tool, or strip it down
to a small example, I need some insights why this happens.
And another question: is this the expected behaviour of definition, to
generate an eta-expanded term instead of a constant?
Also note that the pretty-printer seems not to be impressed by
[[eta_contract=false]] at all, and still prints the eta-contracted
version. (Which makes it even harder to figure out what is going on)
Thanks in advance for any pointers or explanations what is going on,
Peter
theory Scratch
imports
Main
begin
declare [[eta_contract = false]]
experiment
begin
definition "f ≡ length []" (* additional type var *)
(* Looks OK *)
term f (* "f" :: "'a itself ⇒ nat" *)
(* But actually is an eta-expanded term, rather than a simple
constant: *)
ML_val ‹@{term f}› (* Abs ("type", "'a itself", Const
("Scratch.experiment11092848.f", "'a itself ⇒ nat") $ Bound 0) *)
(* And tools expecting constant fail on it *)
ML_val ‹ @{const_name f}› (* Not a logical constant: "local.f" *)
ML_val ‹ @{const f (nat)}› (* Not a logical constant: "local.f" *)
end
Last updated: Apr 19 2024 at 01:05 UTC