theory seq.Seq: added comment

97ca55d8 · Jean-Christophe Filliatre · 51d21a9e · 97ca55d8
Commit 97ca55d8 authored Apr 17, 2015 by Jean-Christophe Filliatre
Hide whitespace changes
Inline Side-by-side

Showing with 4 additions and 0 deletions

theories/seq.why theories/seq.why +4 -0

No files found.
--- a/theories/seq.why
+++ b/theories/seq.why
@@ -147,6 +147,10 @@ end

 (* TODO / TO DISCUSS

+  - add set
+
+      s[i <- v] = s when i < 0 || i >= length s?
+
  - what about s[i..j] when i..j is not a valid range?
    left undefined? empty sequence?