Processing math: 100%

Function type

Type

context X,Y … type
context Γ … context
rule Γ,x : X  y : YΓ  λx.y : XY (lambda abstraction)
rule Γ  f : XYΓ  x : XΓ  fx : Y (function application)

Discussion

Parse Γ,x : X  y : YΓ  λx.y : XY as (Γ,(x : X))  (y : Y)Γ  ((λx.y) : (XY)).

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 'aA' or 'aA'.

Parents

Element of

Link to graph
Log In
Improvements of the human condition