summaryrefslogtreecommitdiff
path: root/transfer/TODO
diff options
context:
space:
mode:
Diffstat (limited to 'transfer/TODO')
-rw-r--r--transfer/TODO2
1 files changed, 2 insertions, 0 deletions
diff --git a/transfer/TODO b/transfer/TODO
index d3a78d49d..6ad3a3428 100644
--- a/transfer/TODO
+++ b/transfer/TODO
@@ -12,6 +12,8 @@
- Simplify taking many arguments of the same type: f : (A,B : Type) -> ...
+- add record extension operator?
+
* Improve interpreter
- More efficient handling of constructor application