Skip to content

v0.6.1

Latest

Choose a tag to compare

@fizruk fizruk released this 25 Jul 04:19
10a267b

This release updates the grammar to match rzk v0.11.1, which adds higher inductive types.

  • Highlight the re-ascription clauses eliminate with and compute with, which replace the eliminator clause of rzk v0.11.0.
  • The into motive of a modal let mod needs no grammar change: into was already a keyword for match.
  • Cover the new syntax in the tests: the circle with a path constructor and both re-ascription clauses.