Commit cf4020c5 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

added lemmas to array.ToSeq

parent 592bda28
......@@ -316,6 +316,14 @@ module ToSeq
forall a: array 'a, l u: int. l < u ->
to_seq a l u = S.cons a[l] (to_seq a (l+1) u)
lemma to_seq_nth:
forall a: array 'a, l i u: int. l <= i < u ->
S.get (to_seq a l u) (i - l) = a[i]
lemma to_seq_length:
forall a: array 'a, l u: int. l <= u ->
S.length (to_seq a l u) = u - l
val to_seq (a: array 'a) (l u: int) : S.seq 'a
requires { 0 <= l && u <= length a }
ensures { result = to_seq a l u }
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