to_has_scalar

Stream: new members

[Winston Yin]

I'm defining a representation k A V (...) := A →ₐ[k] V →ₗ[k] V, and I'm trying to define a to_has_scalar, so it would be convenient to write a • v and define a module structure. However, when I define an instance to_has_scalar (r : representation k A V) : has_scalar A V, subsequent use of the notation a • v results in the error:

maximum class-instance resolution depth has been reached (the limit can be increased by setting option
'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option
'trace.class_instances')

[Winston Yin]

What am I doing wrong?

[Eric Wieser]

Lean has no way to figure out k

[Eric Wieser]

Or for that matter r

[Eric Wieser]

#lint would probably tell you that

[Winston Yin]

You mean the • itself doesn't have enough info about r and k?