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

new library array.ToList

parent 9c2f5b9c
......@@ -307,3 +307,23 @@ module NumOf
function numof (a: array elt) (l u: int) : int = num_of a l u
module ToList
use import int.Int
use import Array
use import list.List
function to_list (a: array 'a) (l u: int) : list 'a
axiom to_list_empty:
forall a: array 'a, l u: int. u <= l ->
to_list a l u = Nil
axiom to_list_cons:
forall a: array 'a, l u: int. l < u ->
to_list a l u = Cons a[l] (to_list a (l+1) u)
val to_list (a: array 'a) (l u: int) : list 'a
ensures { result = to_list 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