summaryrefslogtreecommitdiff
path: root/TODO.md
diff options
context:
space:
mode:
authorSon Ho2022-01-14 13:41:29 +0100
committerSon Ho2022-01-14 13:41:29 +0100
commit74a353f252c70412dd19430ae585b7edbbb836ec (patch)
tree28416dc7eabf0e220ec672019588a619600894ed /TODO.md
parent04a716464d6acd54ada130b7fcd9cf693b532894 (diff)
Update the TODOs
Diffstat (limited to 'TODO.md')
-rw-r--r--TODO.md2
1 files changed, 2 insertions, 0 deletions
diff --git a/TODO.md b/TODO.md
index c3afe870..08fc19ad 100644
--- a/TODO.md
+++ b/TODO.md
@@ -14,6 +14,8 @@
In order to do this, add a symbolic value kind (would make things easier than
adding ad-hoc lookups...): `FunRet`, `FunGivenBack`, `SynthInput`, `SynthGivenBack`
+5. add `mvalue` (meta values) stored in abstractions when ending loans
+
* write an interesting example to study with Jonathan
* add option for: `allow_borrow_overwrites_on_input_values`