Question about producing named instances

Stream: general

[cognivore]

Hi, sorry for a rather silly beginner question.

Consider the following type and class:

inductive K (T: Type) where
| k (t: List T)
| l (t: List Char)
| m

class C (A: Type) where
  Assoc: Type
  ordAssoc: Ord Assoc
  beqK: BEq (K Assoc)

It's trivial to produce ordAssoc by selecting a type, which is Ord.
It's trivial to demonstrate that given Ord T, we can produce BEq (K T).

What I don't understand is how to take the second demonstration (I write it as instance [Ord T]: BEq (K T) where ...) and shove it into beqK.

[Jannis Limperg]

inferInstance and inferInstanceAs are probably what you're looking for.

Maybe this is just a minimisation artifact, but your C looks fishy: the type A is never used.

[cognivore]

It is a minmisation artefact indeed, I'll look at inferInstance (I actually found it, but couldn't understand). In the meantime, @Arthur Paulino has shown me that one can simply name an instance, which makes me feel that even without automatic or semi-automatic resolution, a user should be able to present beqK.

[Jannis Limperg]

Yes, you can name the instance and then the user can give it directly. instance is syntactic sugar for a structure with the @[instance] attribute, so a named instance is roughly the same as @[instance] def myInst [Ord T] : BEq (K T) := .... (In fact, all instances are named; if you don't give a name, Lean will invent one.)

inferInstance gives direct access to typeclass inference. If an instance C A is registered, inferInstanceAs (C A) has type C A (and you don't have to write the instance's name). inferInstance allows you to omit the C A if Lean can figure out from context which class and type you mean.