instance linter

Stream: general

[Yury G. Kudryashov]

Why docs#topological_group_quotient is not a bad instance? It takes subgroup.normal as a non-instance argument.

[Yury G. Kudryashov]

Linter is happy. Is it a bug in the linter or I miss something?

[Patrick Massot]

It probably predates normal being a class and never fires.

[Yury G. Kudryashov]

I wonder why linter doesn't catch it.

[Floris van Doorn]

It is not a bad instance. The variable n occurs in the conclusion, in the proof that the quotient is a group.

protected def topological_group_quotient : ∀ {α : Type u} [_inst_1 : topological_space α] [_inst_2 : group α]
[_inst_3 : @topological_group α _inst_1 _inst_2] (N : @subgroup α _inst_2) (n : N.normal),
  @topological_group (@quotient_group.quotient α _inst_2 N)
    (@quotient_group.quotient.topological_space α _inst_2 _inst_1 N)
    (@quotient_group.group α _inst_2 N n)

[Yury G. Kudryashov]

Thank you for the explanation!