expose class func to top-level

Stream: general

[Zesen Qian]

Hi, how can I expose a function defined in type class to the top-level? i.e., the way to_string is exposed.

[Simon Hudon]

You can do export has_to_string (to_string)

[Zesen Qian]

the function it exposes doesn't seem to the one I want. I have to provide the type parameter.

[Zesen Qian]

I hope I can write to_string 5 instead of to_string nat 5

[Zesen Qian]

ahh sorry, seem in my case, the type inference doesn't work; in other case it works well.

[Simon Hudon]

I think there are two ways of doing that. Either you write a definition in the global namespace where you have fine control over implicit / explicit parameters or you use the following:

class my_algebra (a : Type) :=
  (zero {} : a)

I haven't used it myself but I think it should work.

[Simon Hudon]

(I just tried it. It works)

[Zesen Qian]

thanks! now it works.

[Zesen Qian]

question: how to give the checker a hint for synthesis?

[Simon Hudon]

Do you mean elaboration, i.e. inferring the type that are not explicitly required?

[Zesen Qian]

yes. But in my case it can't be inferred, so I want to give it a hint of the type.

[Simon Hudon]

If your function is foo, @foo makes every implicit parameters (types, type class instances and others) explicit. It's a bit of all or nothing but there are ways to simplify if that comes up too often.

[Simon Hudon]

Sorry, my brain is currently working in Haskell. In Lean, if that comes up too often, you may have to make the parameter explicit. Before you get there, can give some type annotations in the form of (expr : type)

[Simon Hudon]

For example if your function infers a type from its list argument but you provide an empty list, you can write foo ([] : list a) or foo (@nil a)

[Zesen Qian]

yep! I just used annotation and it works well.