Type checking error when using GOSPEL

[mohittkr]

Hello,

It is my first time using GOSPEL. I am trying to write a GOSPEL specification for an OCaml code which uses the Map.Make functor from OCaml. I get the following message when calling the Make functor on some other mli file:

File "lib/util.mli", line 16, characters 4-38:
Error: Type checking error: too few parameters

Line 16 is the following:
val min_binding : 'a t -> key * 'a

I am not sure why I get this error. Any suggestion or comment on this issue will be highly appreciated. Thank you!

[n-osborne]

First, thank you for trying Gospel!

Regarding your issue, without the specification you wrote, it is difficult to tell you what is really going on. Nevertheless, the error message suggest that you have not named enough arguments. Here how the header of the specification should read (modulo choice of name):

val min_binding : 'a t -> key * 'a
(*@ key, a = min_binding t
    (* write the clauses here *)
*)