From 27304bba142f83298689e80fd56b68fd12ba6a86 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Wed, 29 Nov 2023 11:44:02 +0100
Subject: [PATCH] [doc] Spurious TODO removal

---
 doc/interpretation.rst | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/doc/interpretation.rst b/doc/interpretation.rst
index 2c91a80..1d17a5c 100644
--- a/doc/interpretation.rst
+++ b/doc/interpretation.rst
@@ -19,7 +19,7 @@ in the WhyML design and implementation. To quote the author, "[the Why3 team] ha
 
 As CAISAR focuses on artificial intelligence systems, it can
 make some additional assumptions on the nature of the
-inputs, program and users, among the following
+inputs, program and users:
 
 * users will have a basic background on linear algebra, and
   expect CAISAR to reflect this
@@ -65,16 +65,12 @@ Functions
 ~~~~~~~~~
 .. code-block:: whyml
 
-  (** Returns the i-th element of v.
-  TODO: what happens if i > length v ?
-  How do we model matrices? vector of vector? Looks kinda limiting.
-  **)
+  (** Returns the i-th element of v. **)
   function ([]) (v: vector 'a) (i: index) : 'a
 
   function length (v: vector 'a) : int
 
-  (** Returns a vector with the i-th element equals to v1[i] - v2[i].
-  TODO: what happens if length v1 is not length v2? **)
+  (** Returns a vector with the i-th element equals to v1[i] - v2[i]. **)
   function (-) (v1: vector 'a) (v2: vector 'a) : vector 'a
 
   function mapi (v: vector 'a) (f: index -> 'a -> 'b) : vector 'b
-- 
GitLab