Closed n-osborne closed 8 months ago
I imagine the specification dates back from a previous version in which it was possible to write:
type 'a t
(** The type for containers. *)
(*@ model capacity: int
mutable model contents: 'a set
invariant capacity > 0
invariant Set.cardinal contents <= capacity *)
though this has not been valid syntax for quite some time I think.
(I don’t see an example in which it would be still interesting not to name the t
in the invariant at the moment)
Gospel parser allows for:
and
Is the first form necessary? My feeling is that without naming a value of type
t
, there is not much content to give to a type invariant. But maybe I am missing something?This then make the identifier optional in the AST, hence an additional layer of destruction (so to speak) when exploring a type specification and a decision to make about what to do when there is no name (which is useless work if this never happen, and hard to do without having an idea of a potential use case).
Also, I believe the documentation is not up to date: https://github.com/ocaml-gospel/gospel/blob/main/docs/docs/language/type-specifications.md?plain=1#L33