Here, gospel check succeed because 0 is coerced to an integer.
type 'a t
(*@ mutable model contents : 'a sequence *)
val create : unit -> 'a t
(*@ q = create ()
ensures q.contents = Sequence.empty *)
val pop_opt : 'a t -> 'a option
(*@ o = pop_opt q
modifies q.contents
ensures q.contents = match Sequence.length (old q.contents) with
| 0 -> Sequence.empty
| _ -> Sequence.tl (old q.contents) *)
But, in the generated code, 0 is an int:
let next_state cmd__002_ state__003_ =
match cmd__002_ with
| Pop_opt ->
{
contents =
((try
match Ortac_runtime.Gospelstdlib.Sequence.length
state__003_.contents
with
| 0 -> Ortac_runtime.Gospelstdlib.Sequence.empty
| _ ->
Ortac_runtime.Gospelstdlib.Sequence.tl
state__003_.contents
with
| e -> ...
}
Here, gospel check succeed because
0
is coerced to an integer.But, in the generated code,
0
is an int: