Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
function_type [2014/09/17 23:09] nikolaj |
function_type [2014/09/17 23:10] nikolaj |
||
|---|---|---|---|
| Line 9: | Line 9: | ||
| 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)$'. | + | Parse |
| + | |||
| + | $\Gamma,\,x\ :\ X\ \vdash\ y\ :\ Y$ | ||
| + | |||
| + | as | ||
| + | |||
| + | $(\Gamma,\,(x\ :\ X))\ \vdash\ (y\ :\ Y)$ | ||
| ==== Parents ==== | ==== Parents ==== | ||
| === Element of === | === Element of === | ||
| [[Type]] | [[Type]] | ||
