Zulip Chat Archive

Stream: new members

Topic: Argument interpreted as instance?


view this post on Zulip Pedro Minicz (Aug 14 2020 at 16:55):

Why is unfreezeI necessary in the following example? I'd expect hX not to be an instance, as I specified it as an argument ((hX : nonempty X)) not an instance ([nonempty X] or [hX : nonempty X]).

example (hX : nonempty X) (hY : #Y  1) :
  ¬  (f : X  Y) (B : set Y), f '' (f ⁻¹' B)  B :=
begin
  rintros f, A, h₁, h₂,
  refine h₂ (le_antisymm h₁ _),
  intros y hy,
  rw cardinal.le_one_iff_subsingleton at hY,
  cases hY with hY,
  unfreezeI,
  cases hX with x,
  use x,
  specialize hY (f x) y,
  simpa [hY]
end

view this post on Zulip Reid Barton (Aug 14 2020 at 16:56):

The binder type matters to your caller, not to you.

view this post on Zulip Pedro Minicz (Aug 14 2020 at 16:59):

But the type of the lemma is still nonempty ?m_1 → _, so it doesn't seem that the argument would even be given as an instance by the user.

view this post on Zulip Reid Barton (Aug 14 2020 at 17:27):

It wouldn't, but what would happen at a hypothetical use site is not relevant to processing the definition itself.

view this post on Zulip Reid Barton (Aug 14 2020 at 17:29):

The different binder types don't make a difference for the purpose of the definition. hX is treated as an instance because nonempty is a class.

view this post on Zulip Pedro Minicz (Aug 14 2020 at 22:19):

Weird behavior. I'd expect my definition to specify how hX is treated.


Last updated: May 10 2021 at 18:22 UTC