PL type theory notation is wrong.
It's not (Γ ⊢ e : A).
It's (e : Γ ⊢ A).
(hills I contemplate from afar but am unwilling to die on, #1)
7
4
38
Conversation
Replying to
the type of "e" isn't "A", it's "Γ ⊢ A". the context Γ is as important as the type A, and the two belong together.
for example, it matches more nicely with categorical semantics:
e : Γ ⊢ A, so
⟦e⟧ : ⟦Γ⟧ → ⟦A⟧
1
5
Ohh right! What if the term includes variables?
1
1
Show replies