</body>
<news date="MLTT1.">
Martin-Löf's Type Theory with one universe
- using λδ as the theory of expressions.
+ using λδ as theory of expressions.
</news>
<news date="Functional.">
The validation algorithm for λδ as implemented in
according to the following table.
Each component contains its own notation file.
The notation for the relations or functions introduced in each file
- is shown in parentheses.
+ is shown in parentheses (? are placeholders).
</body>
<table name="apps_2_src"/>