simple_array.mlw 134 Bytes
Newer Older
1 2 3 4 5 6 7 8
theory ModelArray

use import map.Map

goal t1 : forall t "model" :map int int, i "model" : int.
   get (set t 0 42) i = get t i

end