1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index d1c77122..6b77ca71 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4674,6 +4674,7 @@ namespace Microsoft.Dafny {
             if (e0 != null) {
               seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqDrop, elType, seq, e0);
             }
+            // if e0 == null && e1 == null, then we have the identity operation seq[..];
             return seq;
           }