Zulip Chat Archive

Stream: general

Topic: subgroup.subtype clobbers subtype notation in namespace


view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 08 2020 at 17:32):

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

view this post on Zulip Chris Hughes (Jul 08 2020 at 17:33):

This might be an easy first C++ PR.

view this post on Zulip Johan Commelin (Jul 08 2020 at 17:33):

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

view this post on Zulip Yury G. Kudryashov (Jul 08 2020 at 20:32):

Or rename it


Last updated: May 14 2021 at 13:24 UTC