diff options
author | Son Ho | 2022-01-14 10:33:02 +0100 |
---|---|---|
committer | Son Ho | 2022-01-14 10:33:02 +0100 |
commit | e6ee5e6fda235e71283c6cccecbfc631457cc949 (patch) | |
tree | 2972d3ba00a67a0e7a282c292b8cdde536ecde75 /TODO.md | |
parent | ed9122c7fc73d77aff5768b27c7f432e89a31d96 (diff) |
Make good progress on end_proj_loans_symbolic
Diffstat (limited to '')
-rw-r--r-- | TODO.md | 4 |
1 files changed, 3 insertions, 1 deletions
@@ -51,7 +51,9 @@ * `ended_proj_loans` (with ghost value) * add a check in function inputs: ok to take as parameters symbolic values with - borrow parameters *if* they come from the "input abstractions" + borrow parameters *if* they come from the "input abstractions". + In order to do this, add a symbolic value kind (would make things easier than + adding ad-hoc lookups...): FunRet, FunGivenBack, SynthInput, SynthGivenBack * make the projected shared borrows more structured? I don't think that's necessary |