Stream: Beginner Questions

Topic: `experiment` bad context for

Robert Soeldner (Jul 09 2023 at 12:35):

I'm trying to use a class definition within an experiment, used to generate latex snippets, but Isabelle rejects the definition with:

Bad context for command "class"⌂

experiment begin
text_raw ‹\DefineSnippet{countable}{›
class countable =
  assumes ex_inj: "∃to_nat :: 'a ⇒ nat. inj to_nat"
text_raw ‹}%EndSnippet›
end

Is there a workaround?

Wolfgang Jeltsch (Jul 09 2023 at 14:26):

With experiment you introduce a kind of throw-away locale, and locale contexts can depend of type variables, values (introduced with fixes), and facts (introduced with assumes), while classes can’t have such dependencies. Maybe it works with notepad, which introduces a throw-away context without any such dependencies, although I can imagine that classes can only be permanent.

Robert Soeldner (Jul 09 2023 at 14:50):

your explanation makes sense. It also prevents the use of notepad. TY :)

Last updated: Apr 28 2024 at 16:17 UTC