Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Interpreting a locale leaving some parameters ...

Email Gateway (Aug 19 2022 at 15:53):

From: Peter Lammich <lammich@in.tum.de>
Hi all,
consider the following boiled down example, where I try to interpret a
locale while leaving some (all) parameters unspecified.

locale foo = fixes x::nat begin
definition "c = x + x"
end

interpretation foo .
*** Illegal free variable(s) in term: x
in constant abbreviation "c"

Why do I get this error message, and can I somehow work around it?
I would have expected an abbreviation of the form "c x == foo.c x" to be
declared.

In my concrete use-case, the locales have no assumptions, and I have to
instantiate some parameters.

Email Gateway (Aug 19 2022 at 15:53):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Peter,

The command interpretation used to accept omitted variables. Over the past years, it has
become a bit stricter about that. Now, you can declare free parameters in a for clause.
Here's an example:

interpretation foo x for x .

Best,
Andreas

Last updated: Apr 19 2024 at 04:17 UTC