Skip to content

Ethos 0.2.2

Choose a tag to compare

@ajreynol ajreynol released this 09 Dec 20:35
· 17 commits to main since this release
59e9ea6

This release of Ethos is associated with the 1.3.2 and 1.3.3 releases of the SMT solver cvc5.

  • The attribute :signature to specify the argument and return types of programs is now required.
  • Evaluation is now forbidden in types of parameters and in the argument types of programs.
  • Higher-order applications of the form (_ f t1 ...tn) no longer desugar based on the desugaring policy for f.
  • Adds builtin list operator eo::list_singleton_elim which converts singleton lists to their (single) element.
  • Adds the operator annotation :right-assoc-non-singleton-nil (resp. :left-assoc-non-singleton-nil). This annotation is similar to :right-assoc-nil but additionally collapses singleton lists to their single elements.