Editing Lambda cube (section)

===λ→===

A typical derivation that can be obtained is<math display="block">\alpha : * \vdash \lambda x : \alpha . x : \Pi x : \alpha . \alpha</math>or with the arrow shortcut<math display="block">\alpha : * \vdash \lambda x : \alpha . x : \alpha \to \alpha</math>closely resembling the identity (of type <math display="inline">\alpha</math>) of the usual λ→. Note that all types used must appear in the context, because the only derivation that can be done in an empty context is <math display="inline">\vdash * : \square</math>.

The computing power is quite weak, it corresponds to the extended polynomials (polynomials together with a conditional operator).<ref>{{Cite journal |last=Schwichtenberg |first=Helmut |author-link=Helmut Schwichtenberg |date=1975 |title=Definierbare Funktionen imλ-Kalkül mit Typen |journal=[[Archiv für Mathematische Logik und Grundlagenforschung]] |volume=17 |issue=3–4 |pages=113–114 |doi=10.1007/bf02276799 |s2cid=11598130 |issn=0933-5846 |language=DE}}</ref>