From b712795d5b8aa1bf831a80b3a410c35946fcbce0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 23 Feb 2022 19:02:11 +0100
Subject: Add a comment

---
 src/PureToExtract.ml | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

(limited to 'src/PureToExtract.ml')

diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 2a47eb6f..42a4c589 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -286,7 +286,24 @@ let names_map_add_assumed_function (id_to_string : id -> string)
     We do this in an inefficient manner (by testing all indices starting from
     0) but it shouldn't be a bottleneck.
     
-    [append]: appends an index to a string
+    Also note that at some point, we thought about trying to reuse names of
+    variables which are not used anymore, like here:
+    ```
+    let x = ... in
+    ...
+    let x0 = ... in // We could use the name "x" if `x` is not used below
+    ...
+    ```
+    
+    However it is a good idea to keep things as they are for F*: as F* is
+    designed for extrinsic proofs, a proof about a function follows this
+    function's structure. The consequence is that we often end up
+    copy-pasting function bodies. As in the proofs (in assertions and
+    when calling lemmas) we often need to talk about the "past" (i.e.,
+    previous values), it is very useful to generate code where all variable
+    names are assigned at most once.
+    
+    [append]: function to append an index to a string
  *)
 let basename_to_unique (names_set : StringSet.t)
     (append : string -> int -> string) (basename : string) : string =
-- 
cgit v1.2.3