naming X : S for a structure S

Stream: general

[Dean Young]

What is the best way to use the notation "x : S" for a structure S? For instance, suppose I want to use that notation here:

structure magma where
  X : Type
  μ : X → X → X
  α : (x : X) → (y : X) → (z : X) → μ (μ x y) z = μ x (μ y z)

[Eric Wieser]

What's your question?

[Eric Wieser]

Are you asking whether you can write m : magma? The answer is yes.

[Kyle Miller]

There's also potentially the question of whether given S : magma you can write x : S for x : S.X. You can write a docs4#CoeSort instance.

[Dean Young]

"whether you can write m : magma" yes that's my question ... but also how does it know the meaning of m : magma? And when does that work?

[Reid Barton]

Because you just defined what the type magma is...? Is this really the question you want to ask?

[Logan Murphy]

Once magma is defined with structure, it becomes a type, i.e. in this case we have magma : Type 1, so m : magma is completely sensible

[Logan Murphy]

note that structure is essentially just inductive with a single constructor, so your definition is the same as

inductive magma
| mk (X : Type) (μ: X → X → X) (α :  (x : X) → (y : X) → (z : X) → μ (μ x y) z = μ x (μ y z))  : magma

given this definition, would you expect m : magma to fail somehow?