summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-07 13:57:47 +0100
committerSon Ho2022-01-07 13:57:47 +0100
commit4e2dd5806fe41275bf8c037b9071175e51c88c62 (patch)
tree8f121b8a1a42506dcfa82eedb001c6aa9415b5b2 /src
parent2ee5357216cc5a620dbe6d091b0081d419951a4e (diff)
Add a high-level comment
Diffstat (limited to '')
-rw-r--r--src/Values.ml8
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: