Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
function_type [2014/09/17 23:12]
nikolaj
function_type [2014/09/17 23:12] (current)
nikolaj
Line 7: Line 7:
  
 ==== Discussion ==== ==== Discussion ====
-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 ${\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))}}$. 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$'.
  
 ==== Parents ==== ==== Parents ====
 === Element of === === Element of ===
 [[Type]] [[Type]]
Link to graph
Log In
Improvements of the human condition