Why `Function` is special

Stream: general

[Schrodinger ZHU Yifan]

inductive Test := | T
inductive Function := | F

def Test.id (_ : Test) : Nat := 1
def Function.id (_ : Function) : Nat := 1

#eval Test.T.id

#eval Function.F.id

Will give

schrodinger@Yifans-MacBook-Air /tmp % lean test.lean
1
test.lean:9:6: error: invalid field notation, function 'Function.id' does not have argument with type (Function ...) that can be used, it must be explicit or implicit with a unique name

[Floris van Doorn]

docs#Function.id already exists?

[Floris van Doorn]

Apparently not, but it is probably related to the fact that Function is already an existing namespace...

[Floris van Doorn]

It's also a very special namespace: since you can use dot notations on any function, and it will use the declaration in the Function namespace. For example, the following codesnippet uses Function.comp:

example {α} (f g : α → α) : f.comp g = f.comp g := rfl

This means that if you use dot notation in the Function namespace, Lean expects a function, not something of type Function.

TL;DR: rename the type Function