Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
function_type [2014/09/17 23:10] nikolaj |
function_type [2014/09/17 23:12] nikolaj |
||
---|---|---|---|
Line 7: | Line 7: | ||
==== Discussion ==== | ==== Discussion ==== | ||
+ | Parse ${\large\frac{\Gamma,\,x\ :\ X\ \vdash\ y\ :\ Y}{\Gamma\ \vdash\ \lambda x.\,y\ :\ X\to Y}}$ as ${\large\frac{(\Gamma,\,(x\ :\ X))\ \vdash\ (y\ :\ Y)}{\Gamma\ \vdash\ ((\lambda x.\,y)\ :\ (X\to Y))}}$. | ||
+ | |||
Note that from the wikis perspective, the described type theory is an object language and in it, the context $\Gamma$ is a list of judgements, alla '$a:A$'. That's not to be confused with the context of the meta language (blue boxes) where we also use the notations '$a$...$A$' or '$a\in A$'. | Note that from the wikis perspective, the described type theory is an object language and in it, the context $\Gamma$ is a list of judgements, alla '$a:A$'. That's not to be confused with the context of the meta language (blue boxes) where we also use the notations '$a$...$A$' or '$a\in A$'. | ||
- | |||
- | Parse | ||
- | |||
- | $\Gamma,\,x\ :\ X\ \vdash\ y\ :\ Y$ | ||
- | |||
- | as | ||
- | |||
- | $(\Gamma,\,(x\ :\ X))\ \vdash\ (y\ :\ Y)$ | ||
==== Parents ==== | ==== Parents ==== | ||
=== Element of === | === Element of === | ||
[[Type]] | [[Type]] |