when is a structure an inductive?

Stream: general

[Scott Morrison]

Sometimes when you use structure ..., Lean decides to create an inductive ... instead. Is there a description available of how it decides this?

[Gabriel Ebner]

What do mean by "sometimes"? Lean always creates an inductive for a structure.

[Scott Morrison]

ah, but doesn't create "structure notation" and projections.

[Scott Morrison]

(and when you #print the structure, it shows inductive ... rather than structure ...)

[Scott Morrison]

Unfortunately my example is on a messy branch. I will see if I can extract it.

[Scott Morrison]

In branch#alg_equiv_old_structure_cmd, in algebra/algebra/basic.lean, I have:

/-- An equivalence of algebras is an equivalence of rings commuting with the actions of scalars. -/
structure alg_equiv (R : Type u) (A : Type v) (B : Type w)
  [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B]
  extends to_ring_equiv : A ≃+* B :=
(commutes' : ∀ r : R, to_ring_equiv.to_fun (algebra_map R A r) = algebra_map R B r)

#print alg_equiv

and it is saying inductive alg_equiv ....

[Scott Morrison]

(and structure syntax, i.e. { to_ring_equiv := ..., commutes' := ... }, is not available)

[Gabriel Ebner]

Hmm, this looks like a bug. But the example looks fairly innocent, I wonder why we haven't run into it so far.

[Scott Morrison]

Okay, I need to head off this evening, but I will think about it more later. Thanks!