## Stream: general

### Topic: subgroup.subtype clobbers subtype notation in namespace

#### Kevin Buzzard (Jul 08 2020 at 17:20):

Is the below expected behaviour? It is what tripped up @Scott Morrison here.

import group_theory.subgroup

#check @subgroup.subtype

-- subgroup.subtype : Π {G : Type u_1} [_inst_1 : group G] (H : subgroup G), ↥H →* G

namespace subgroup

example : 2 + 2 = 5 :=
begin
let Z := {n : ℕ // n = n},
/-
type mismatch at application
subtype (λ (n : ℕ), n = n)
term
λ (n : ℕ), n = n
has type
ℕ → Prop : Type
but is expected to have type
subgroup ?m_1 : Type ?
state:
⊢ 2 + 2 = 5
-/
end

end subgroup


#### Johan Commelin (Jul 08 2020 at 17:32):

Can this be fixed in C++ by making { // } notation for _root_.subtype explicitly?

#### Chris Hughes (Jul 08 2020 at 17:33):

This might be an easy first C++ PR.

#### Johan Commelin (Jul 08 2020 at 17:33):

@Kevin Buzzard Another fix might be to make submodule.subtype a protected def

#### Yury G. Kudryashov (Jul 08 2020 at 20:32):

Or rename it

Last updated: May 14 2021 at 13:24 UTC