Zulip Chat Archive

Stream: general

Topic: unfold class


view this post on Zulip blackxv (Nov 16 2020 at 07:24):

hello everyone,
lemma Q2b : ¬is_total (set ℤ) (λ A B, A ⊆ B)
how to unfold is_total?
thank you in advance!

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 07:27):

Does unfold is_total (in tactic mode) work?

view this post on Zulip Alex J. Best (Nov 16 2020 at 07:28):

is_total is a class, but you can do

lemma Q2b : ¬is_total (set ) (λ A B, A  B) := begin
  intro h,
  cases h,
end

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 07:28):

If not then try cases h if h : is_total ...

view this post on Zulip blackxv (Nov 16 2020 at 07:31):

cases h works, thank you!

lemma Q2b : ¬is_total (set ) (λ A B, A  B) := begin
  intro h,
  cases h,
end

Are there some addional plugs to install in order to show lean code in a special style here?

ok yeah, ```works.

view this post on Zulip Alex Peattie (Nov 16 2020 at 07:54):

Code formatting is explained here: #backticks :smile:


Last updated: May 14 2021 at 03:27 UTC