two functions with the same name

Stream: new members

[Ali Sever]

Is there a reason why lean doesn't let me make two functions with the same name? Even if they take different arguments?

[Chris Hughes]

It's confusing, and could even lead to people thinking they've proved something, when they've actually proved something about a function with the same name. You can always use namespaces.

[Mario Carneiro]

You can have two functions in different namespaces with the same name, where both namespaces are open at once, and lean will use the type to disambiguate

[Mario Carneiro]

The basic reason why is because lean needs a name for the function, one that is not ambiguous, and if you overload it what will that name be? How can you refer to it precisely?

[Ali Sever]

I know I should be using Pi types for this sort of thing, but my two functions take in a different amount of arguments, so I think I might have to use if then else.

[Mario Carneiro]

You can also use default values and optional arguments to make a single definition have varying number of arguments

[Kevin Buzzard]

Also note that + is kind of like several functions with the same name -- and looking at the types of the inputs is exactly how Lean decides which function to actually use.