Instance field in structure/class

Stream: lean4

[Andrea Laretto]

Is it possible to have a field in a structure (or a class) that is provided as instance of some class? For example, this can be done in Agda with the {{eqA}} field here

[Andrea Laretto]

I think I might have found the answer to this problem by having [fieldName : type] in instance declarations, but still seems to behave badly with typeclass resolution in the subsequent fields of the class...

[Kevin Buzzard]

The square brackets in the definition just mean "treat this as a typeclass in the rest of the definition". (this is not exactly right: see Eric's comment below). You need to explicitly make the instance directly after the definition and then you should be ok

[Andrea Laretto]

That makes sense, thanks!
p.s., is there an easy way to explicitly supply instances (or implicit arguments, for that matter) that isn't using @ and then providing every single argument?

[Yaël Dillies]

The f (arg := value_of_the_arg) syntax

[Andrea Laretto]

Thanks! I'll try it out but I don't recall ever seeing it in any of the tutorials (e.g. TPIL4, the Lean 4 manual)...

[Eric Wieser]

Kevin Buzzard said:

The square brackets in the definition just mean "treat this as a typeclass in the rest of the definition".

This half of your comment isn't true, it gets treated as a typeclass even without the []. The []s mean "treat this as an instance argument in the .mk constructor function".

[Eric Wieser]

That is, this works fine:

structure SureWhyNot where
  X : Type
  i : HAdd X X X
  h (x : X) : x + x = x

Lean knew to use i as an instance to resolve the + that follows.

[Andrea Laretto]

Oh, that's true! Removing the brackets still makes everything go through, so I guess it is automatically provided as instance. The explaination on the constructor also makes sense; in the case of typeclasses I guess it tries to infer them so that they can be left out.

[Eric Wieser]

In the same vein, you can write {X : Type*} to make that argument to .mk implicit

[Andrea Laretto]

Eric Wieser said:

In the same vein, you can write {X : Type*} to make that argument to .mk implicit

What does Type* refer to here? Is it specific syntax?

On that note, I have another small question on the topic of instances: how do I package a term with an instance on it (e.g., basically a sigma type in which the second part is basically a class) in such a way that the instance is "picked up" when the term is brought into scope? Is there an idiomatic way of doing this or should I just unpack it λ ⟨X,_⟩ ⟨Y,_⟩ => ...<place where the instance is used> like this?

[Kevin Buzzard]

Type* means "a type in any universe". Lean has an infinite heirarchy of types: the type of Type is Type 1, the type of Type 1 is Type 2 etc.

[Andrea Laretto]

Is Type* more or less a shorthand for implicitly quantifying (only once) over any universe level? I don't recall ever seeing this in any Lean book...

[Eric Rodriguez]

Type* is a shorthand for universe u ; variable {A : Type u} with a new u for every use.

[Eric Rodriguez]

This is mathlib-defined syntax, as far as I understand.