Function type
Type
context | X,Y … type |
context | Γ … context |
rule | Γ,x : X ⊢ y : YΓ ⊢ λx.y : X→Y (lambda abstraction) |
rule | Γ ⊢ f : X→YΓ ⊢ x : XΓ ⊢ fx : Y (function application) |
Discussion
Parse Γ,x : X ⊢ y : YΓ ⊢ λx.y : X→Y as (Γ,(x : X)) ⊢ (y : Y)Γ ⊢ ((λx.y) : (X→Y)).
Note that from the wikis perspective, the described type theory is an object language and in it, the context Γ 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∈A'.