Difference between function and dependent type

Stream: new members

[Gabriel Soranzo]

In reading the book "Theorem proving in Lean 4" I met the expression def F (α : Type u) : Type u := Prod α α. It seems to me very similar to a function like def h: Type u → Type u:= fun α => Prod α α.

Do these two expressions are the same and if not what is the difference?

[Yaël Dillies]

They are the same, but the Lean commands used to define do slightly different things

[Yaël Dillies]

def F (α : Type u) : Type u := Prod α α

creates an "equational lemma"

theorem F (α : Type u) : F α = Prod α α := rfl

[Yaël Dillies]

def h : Type u → Type u := fun α => Prod α α

instead creates the equational lemma

theorem h : h = fun α => Prod α α := rfl

[Gabriel Soranzo]

I think I'm to far to begginner in Lean to understand the difference... In first approximation, if I understand well: it's the same.

[Yaël Dillies]

More or less, yeah. You can leave it at that