structure question

Stream: general

[Kevin Buzzard]

I was just checking I'd got symmetry working with ne:

attribute [symm] ne.symm

/-
class zero_ne_one_class (α : Type u) extends has_zero α, has_one α :=
(zero_ne_one : 0 ≠ (1:α))
-/
example (R : Type) [zero_ne_one_class R] : (1 : R) ≠ 0 :=
begin
  symmetry,
  exact zero_ne_one,
end

and this worked fine. But actually I didn't expect it to work, I expected Lean to moan that it couldn't find an instance of has_zero R etc. The zero_ne_one_class instance seems to have magicked them up!

But that's weird, because this fails:

import topology.algebra.ring

/-
class topological_ring extends topological_add_monoid α, topological_monoid α : Prop :=
(continuous_neg : continuous (λa:α, -a))
-/

example (S : Type) [topological_ring S] : (0 : S) = 0 := rfl
/-
failed to synthesize type class instance for
S : Type
⊢ topological_space S

failed to synthesize type class instance for
S : Type
⊢ ring S

failed to synthesize type class instance for
S : Type,
_inst_1 : topological_ring S
⊢ has_zero S

failed to synthesize type class instance for
S : Type,
_inst_1 : topological_ring S
⊢ has_zero S

-/

Structures are still a bit weird to me. Is this got something to do with the "old" structure command or is this yet another weirdness about structures?

[Kevin Buzzard]

Aah, I see:

class topological_add_monoid (α : Type u) [topological_space α] [add_monoid α] : Prop :=
(continuous_add : continuous (λp:α×α, p.1 + p.2))

[Kevin Buzzard]

"Extends" gets done automatically, the square bracket stuff doesn't. And there is no doubt some great reason involving diamonds or something which means that it can't extend them.

[Johan Commelin]

Exactly