I am a beginner in type theories. I have a basic question about the notion of context. It is commonly found in a textbook on type theories that a context (sometimes also called an environment) is defined as a sequence of variable declarations (or assumptions) such as $\langle x_1:C_1,x_2:C_2,...,x_n:C_n\rangle$. But I find in my handouts that the following sequence is also a valid context:
$\Gamma=\langle\mathbb{N}:Type, 1:\mathbb{N}, suc:\mathbb{N}\rightarrow\mathbb{N}, suc(suc 1):\mathbb{N}\rangle$
My question is: none of the expressions in $\Gamma$ contains any free variable, so how should I understand the definition of context as a sequence of variable declarations?
Here is the text that I am referring to in my handout:
An empty context $\langle\ \rangle$ can be extended by a new type $\mathbb{N}$. We get the following judgment: $$\langle\mathbb{N}:Type\rangle\vdash\mathbb{N}:Type.$$ This judgement show that the context '$\mathbb{N}:Type$' is legal. To indicate this, we write: $$\langle\mathbb{N}:Type\rangle\vdash ok.$$ Next, we can extend this context with a declaration of a natural number, like 'one'. We get the following judgment: $$\langle\mathbb{N}:Type,1:\mathbb{N}\rangle\vdash1:\mathbb{N}.$$ This context is also legal: $$\langle\mathbb{N}:Type,1:\mathbb{N}\rangle\vdash ok.$$ Next we want to introduce the type of a notion of successor function. Using $\rightarrow$, it follows that: $$\langle\mathbb{N}:Type, 1:\mathbb{N},\mathbb{N}\rightarrow\mathbb{N}:Type\rangle\vdash ok.$$