Skip to content

v1.4.0
Compare
Choose a tag to compare
@valis valis released this 29 Jun 09:48
· 1415 commits to master since this release
v1.4.0
264c836

Language updates:

  • Implicit lambdas.
  • Tests directory can be used to store files with tests, examples, and other code which is not a part of the library.
  • Improved pretty printer: if some definition is not available in the current context, it will be replaced with its full name.
  • REPL
  • Arend now supports unicode symbols through aliases.
  • Equality between disjoint constructors is now considered empty.
  • Added support for incomplete lambdas, let expressions, and tuples.
  • Implemented tail call optimization.

API:

  • Goal solvers can be used to replace goals with expressions.
  • Arend UI allows meta definitions to interact with the user.
  • Level solvers can be used to automatically prove that a type belongs to a certain homotopy level.
  • Number type-checker can be used to elaborate numerical literals to arbitrary expressions.
  • User data in definitions can be used to store arbitrary user data.
  • User data in ContextData can be used to pass information between meta definitions.
Assets 5
Loading