libray seq: added a FIXME

parent 4548a86e
......@@ -22,6 +22,7 @@ module Seq
forall s: seq 'a. 0 <= length s
val function get (seq 'a) int : 'a
(* FIXME requires { 0 <= i < length s } *)
(** `get s i` is the `i+1`-th element of sequence `s`
(the first element has index 0) *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment