I've done the first 3 chapters of the lean tutorial, and I've already done a few proofs in propositional logic.
Now I'm trying to go back a bit and ask myself dumb questions.
My understanding is that:
constant A : Type. A is a term, Type is the type of A.constant a : A.constant B : A -> Type, which is sugar for constant B' : Π (a : A), TypeBut this understanding is clearly wrong, for this code doesn't typecheck:
constant A : Type
constant a : A
constant B : A -> Type
constant B' : Π (a : A), Type
constant C : Π (b : B), Type
constant C' : Π (B : A), (Π (b : B), Type)
constant C'' : B -> Type
All lines beginning constant C, that is line 9, 11 and 13 throw an error error: type expected at B
Why? I suspect that not all terms can become types. I suspect that terms whose types depend on other types can't become types. Why?
The problem with the first type error in
constant C : Π (b : B), Type
is that you cannot say b : B, because B is a function (without definition) of type A -> Type, i.e. B is a value, not a type.
It doesn't make sense to make a claim like b : 1 or b : "xyz" or b : (λ a : A, Type).
E.g. the following would work, since B a : Type:
constant C : Π (b : B a), Type
The second type error in
constant C' : Π (B : A), (Π (b : B), Type)
stems from the fact that it is not known that B is a type, all we know about B is that it is some value (inhabitant) of type A. To be able to use B that way, you'll need something like this:
constant C' : Π (B : Type), (Π (b : B), Type)
i.e. we explicitly say B is a type.
constant C'' : B -> Type
The reason this fails to typecheck is the same as in the first case. B is a function value, while we need a type here -- this is why constant B : A -> Type works.