diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Values.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Values.ml b/src/Values.ml index c9dff56a..53851cea 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -473,6 +473,14 @@ and aborrow_content = > } ``` + + Note that we could use AIgnoredMutLoan in the case the borrow id is not + None, which would allow us to simplify the rules (to not have rules + to specifically handle the case of AIgnoredMutBorrow with Some borrow + id) and also remove the AEndedIgnoredMutBorrow variant. + For now, the rules are implemented and it allows us to make the avalues + more precise and clearer, so we will keep it that way. + TODO: this is annoying, we are duplicating information. Maybe we could introduce an "Ignored" value? We have to pay attention to two things: |