mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
9 lines
110 B
Plaintext
9 lines
110 B
Plaintext
theory ModelArray
|
|
|
|
use map.Map
|
|
|
|
goal t1 : forall t: map int int, i: int.
|
|
get (set t 0 42) i = get t i
|
|
|
|
end
|