From 4e2dd5806fe41275bf8c037b9071175e51c88c62 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 7 Jan 2022 13:57:47 +0100
Subject: Add a high-level comment

---
 src/Values.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src')

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:
-- 
cgit v1.2.3