universe polymorphism in arguments

Stream: new members

[Jakub Nowak]

I don't understand, why this doesn't work? Why is it not possible to infer u = 0?

example (h : (α : Type u) → (a : α) → α) := by
  let := @h Nat 0

[Aaron Liu]

see #new members > Reasoning about functions

[Jakub Nowak]

Ah, I think I know. u is parameter of my unnamed example def, right?
Is it possible to have universe polymorphic argument? I guess not?

[Aaron Liu]

why do you think it should be possible to infer u = 0

[Aaron Liu]

Jakub Nowak said:

Ah, I think I know. u is parameter of my unnamed example def, right?
Is it possible to have universe polymorphic argument? I guess not?

yes that is not allowed by Lean's type theory, you can only have universe-polymorphic definitions