Zulip Chat Archive

Stream: general

Topic: what does . mean?


view this post on Zulip Kenny Lau (Apr 16 2018 at 01:25):

type mismatch at application
  Exists.intro property_w property_h
term
  property_h
has type
  (λ (a : G), left_coset a (stab G X x)) property_w = val
but is expected to have type
  . (λ (y : G), (λ (a : G), left_coset a (stab G X x)) y = _x) property_w

view this post on Zulip Kenny Lau (Apr 16 2018 at 01:25):

what does the mystic . on the start of the last line mean?

view this post on Zulip Simon Hudon (Apr 16 2018 at 01:27):

That looks like a typo in the error message. If you ignore it, does the expression make sense?

view this post on Zulip Kenny Lau (Apr 16 2018 at 01:27):

a typo in the error message?

view this post on Zulip Simon Hudon (Apr 16 2018 at 01:27):

Yeah, someone had to type that error message in the code. They may have made a mistake.

view this post on Zulip Kenny Lau (Apr 16 2018 at 01:29):

it still doesn't make much sense

view this post on Zulip Kenny Lau (Apr 16 2018 at 01:29):

theorem orbit_equiv_stab_cosets (x : X) : nonempty (orbit G X x ≃ left_cosets (stab G X x)) :=
nonempty.intro $
@equiv.of_bijective _ _ (orbit_to_stab_cosets G X x) $
and.intro
  (λ ⟨y1, g1, h1⟩ ⟨y2, g2, h2⟩ H, subtype.eq $ h1.symm.trans $ (((set.set_eq_def _ _).1 $ subtype.mk.inj H) g1).1 h1)
  (λ ⟨gH, g, h⟩, ⟨⟨g ● x, _, rfl⟩, subtype.eq $ h ▸ (set.ext $ λ z, by simp [mem_left_coset_iff]; admit)⟩)

view this post on Zulip Kenny Lau (Apr 16 2018 at 01:29):

I don't have property_h anywhere

view this post on Zulip Simon Hudon (Apr 16 2018 at 01:32):

Do you have a proof of an existential quantification somewhere in there?

view this post on Zulip Mario Carneiro (Apr 16 2018 at 01:52):

the . there is the pp printing of an inaccessible pattern. I'm not exactly sure what you are looking at, but you can safely ignore it


Last updated: May 14 2021 at 13:24 UTC