Email Gateway (Aug 22 2022 at 09:49): Email Gateway (Aug 22 2022 at 09:49):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
given a function definition like this:
fun f :: "'a => 'a" where "f x = x"
the info record of the function can be obtained with the function constant
Function.get_info @{context} @{term "f"}
However, now consider the same definition in the context of a locale
with a fixed parameter:
locale foo = fixes a :: 'a
begin
fun f :: "'a => 'a" where "f x = x"
Now "f" (or rather "local.f") is just an abbreviation for "foo.f a", and
one would have to passe "foo.f a" into Function.get_info, not, as I
would expect, "foo.f". This makes it very difficult to obtain the info
record when given a function application like "f 2", i.e. "foo.f a 2",
because there is no way of knowing how many arguments to strip away from
"foo.f a 2".
When leaving the context with "end", I would have expected it to be
exported in some way (e.g. by adding the locale assumptions to all the
theorems). This does not happen – the function is deleted from the
context completely.
Is this behaviour known?Is it intentional? Is there some reasonable way
of changing it to what I described?
Cheers,
Manuel
Last updated: Apr 25 2024 at 20:15 UTC