Type Classes syntax question

Stream: new members

[Rado Kirov]

What's the difference between these two ways of receiving a type class instance:

def double1 [i : Add a] (x : a) : a := i.add x x
def double2 [Add a] (x : a) : a := Add.add x x

Both seem to work the same?

[Kyle Miller]

They work the same.

The second is more idiomatic, while the first lets you write double (i := myInstance) with named arguments.

[Rado Kirov]

Got it. Is this a good place to give feedback for theorem_proving_in_lean4. The second one came out of nowhere in https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html#numerals and threw me off.

[Rado Kirov]

Also it seems that the examples there work with nat_lit 1 replaced with 1, so maybe Lean has improved since it was written.

[Kyle Miller]

Yeah, Lean improved and nat_lit doesn't seem to be needed very often anymore.

[Kyle Miller]

It seems worth filing an issue: https://github.com/leanprover/theorem_proving_in_lean4/issues

It should have a word about how [Add a] is like [inst : Add a] where inst is a fresh name.

The idea here is that instance implicits tend to always be passed around using instance implicit arguments, so you very rarely will refer to them directly. The syntax makes it easy to not have to provide a name.

[Eric Wieser]

Kyle Miller said:

Yeah, Lean improved and nat_lit doesn't seem to be needed very often anymore.

Isn't it supposed to be there on principle?

[Rado Kirov]

The distinction is meaningful, but specifically in https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html#numerals

at the end, when it says

The second argument is often a variable as in the example above, or a raw natural number.

I get the code to compile without nat_num

[Rado Kirov]

I am sure there are still some other places where nat_num is needed.