Skip to content

0.2.0

Compare
Choose a tag to compare
@shym shym released this 06 Oct 12:46
· 109 commits to main since this release
eef2a72

This release adds two main features, a gospel dumpast command and a gospel.ppx ppx rewriter to display gospel contents as documentation with odoc.

Some minor extensions have been added to the language itself:

  • a with construct to name a variable in type invariants referring to a value of the specified type,
  • int literals,
  • anonymous functions now support both patterns in arguments and return type annotations,
  • unit result in function header,
  • constants can now be referenced in specifications,
  • infix operators are now accepted in specification headers.

Parser, preprocessor and error messages have been improved. In particular the preprocessor can now handle large files and locations are properly tracked.
Pattern matches are now checked for exhaustiveness and redundancy.
A number of improvements and bugfixes in the type checker.
Some minor modifications in the Gospel standard library.
Documentation has been revised.