Stream: Beginner Questions

Topic: Locale assumptions


view this post on Zulip Josh Chen (May 26 2020 at 19:41):

Is there a binding to get locale assumptions internally? So if I have e.g.

locale my_loc =
fixes A
assumes "pred A"
begin

lemma my_lem:
  notes ???
...

what do I write for ??? in order to refer to "pred A"?

view this post on Zulip Kevin Kappelmann (May 26 2020 at 19:52):

Is this what you are looking for?

locale my_loc =
fixes A
assumes my_asm: "pred A"
begin

lemma my_lem:
  notes my_asm

view this post on Zulip Josh Chen (May 26 2020 at 19:55):

Yeah that's what I do. Just wondering if there is a predefined name. Thanks!

view this post on Zulip Kevin Kappelmann (May 26 2020 at 19:57):

What happens if you put print_theorems below begin?

view this post on Zulip Kevin Kappelmann (May 26 2020 at 19:59):

Seems like you could quote my_loc_def, which of course I would not recommend ^^


Last updated: Mar 29 2024 at 01:04 UTC