function type

Stream: new members

[Holly Liu]

what's the difference between functions of type Π and of type λ?

[Eric Rodriguez]

Π declares a function type, λ introduces it to prove things. Π is ∀, and λ is intros, basically

[Eric Rodriguez]

for example: def id' : Π α : Type*, Type* := λ α, α

[Johan Commelin]

In other words, a term of shape λ _, _ has a type of shape Π _, _.

[Holly Liu]

ok, thanks

[Kevin Buzzard]

Pi A, B is how the computer scientists write Hom(A,B) and lambda is how they write $\mapsto$