exists is a reserved keyword

[n-osborne]

The following gospel specification:

val exists : ('a -> bool) -> 'a list -> bool
(*@ b = exists p xs *)

will raise:

$ gospel check file.mli
File "file.mli", line 2, characters 8-14:
2 | (*@ b = exists p xs *)
            ^^^^^^
Error: Syntax error.

The problem is that exists is a reserved keyword, but also the classical name for the exists function.

[shym]

This extends to all the keywords, with in particular forall and pure as natural names for functions we would want to specify.