theory seq.Seq: alternate name get for []

parent eb16012a
......@@ -37,6 +37,9 @@ theory Seq
(** [s[i]] is the ([i]+1)-th element of sequence [s]
(the first element has index 0) *)
function get (s: seq 'a) (i: int) : 'a =
s[i]
(** equality *)
predicate (==) (s1 s2: seq 'a) =
......
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