Zulip Chat Archive

Stream: general

Topic: unfold class


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!

Kevin Buzzard (Nov 16 2020 at 07:27):

Does unfold is_total (in tactic mode) work?

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

Kevin Buzzard (Nov 16 2020 at 07:28):

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

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.

Alex Peattie (Nov 16 2020 at 07:54):

Code formatting is explained here: #backticks :smile:


Last updated: Dec 20 2023 at 11:08 UTC