## Stream: general

### Topic: what does . mean?

#### 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


#### Kenny Lau (Apr 16 2018 at 01:25):

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

#### 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?

#### Kenny Lau (Apr 16 2018 at 01:27):

a typo in the error message?

#### 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.

#### Kenny Lau (Apr 16 2018 at 01:29):

it still doesn't make much sense

#### 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)⟩)


#### Kenny Lau (Apr 16 2018 at 01:29):

I don't have property_h anywhere

#### Simon Hudon (Apr 16 2018 at 01:32):

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

#### 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