Skip to content

Commit

Permalink
REMOVE ME: Change hashtbl to use List.filter_map and avoid mixing Lis…
Browse files Browse the repository at this point in the history
…ts and Sequences
  • Loading branch information
jmid committed Dec 5, 2024
1 parent 63109c8 commit 93ea93a
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions plugins/qcheck-stm/test/hashtbl.mli
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ val find_opt : ('a, 'b) t -> 'a -> 'b option

val find_all : ('a, 'b) t -> 'a -> 'b list
(*@ bs = find_all h a
ensures bs = Sequence.filter_map (fun (x, y) -> if x = a then Some y else None) h.contents *)
ensures bs = List.filter_map (fun (x, y) -> if x = a then Some y else None) h.contents *)

val mem : ('a, 'b) t -> 'a -> bool
(*@ b = mem h a
Expand All @@ -64,7 +64,7 @@ val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit
val filter_map_inplace : ('a -> 'b -> 'b option) -> ('a, 'b) t -> unit
(*@ filter_map_inplace f h
modifies h
ensures h.contents = Sequence.filter_map
ensures h.contents = List.filter_map
(fun (x,y) -> match f x y with
| None -> None
| Some b' -> Some (x, b'))
Expand Down

0 comments on commit 93ea93a

Please sign in to comment.