Standard Library

Gospel provides a set of useful types, functions and predicates that you can use in your specifications. To get you started as quickly as possible, this standard library tries to mimic conventions and naming that exist in the OCaml standard library.

Please keep in mind that it only contains logical symbols though, and should not be confused with those provided by the OCaml standard library (which you are not allowed to use in specifications!).

The interface for the Gospel standard library can be seen here or directly in the repository.