Arend

• Properties in \Sigma-types
• Definition parameters are visible in the \where block
• Global level declarations
• Infix patterns
• Axioms
• Box expressions
• Property parameters

• Improved performance
• Inference of unique implicit arguments
• Coercion between paths and functions
• A convenient syntax for defining HITs and pattern matching on them

• Type synonyms
• Arrays
• Pattern matching in lambdas and \let expressions
• Multiple level parameters in definitions
• Ability to change levels in class extensions
• Improved inference of implicit arguments of function types

A few bug fixes

Language updates:

• Built-in finite types
• \default implementations
• \coerce to function types
• \coerce for fields and constructors
• \have declaration
• Dot-syntax for dynamic definitions
• Added more computational rules for Nat.+ and Nat.- functions

API:

• Pattern typechecker

• String literals, which can be used in meta code
• Meta resolvers, which can be used to modify the scoping rules for meta definitions
• \strict parameters
• Improved performance
• Defined metas
• Libraries can be loaded from zip archives without unpacking

• Improved implicit arguments inference.
• Fixed a bug aliases in namespace commands.
• Fixed a bug with defined constructors.

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.

New features and updates:

• Implemented language extensions
• Show conditions in goals

New features and updates:

• Implemented pattern matching on idp.
• New keyword \noclassifying.
• The type of a field can be overridden with a subtype in a subclass using new keyword \override.
• Variables can be eliminated in \case expressions now.
• Implemented constructor synonyms.
• It is possible now to implement fields using pattern matching.
• We decided to make \Prop proof relevant in general (but it is still proof irrelevant in some cases).
• Now, fields and implementations in a class are typechecked in the order they are specified (before now implementations were typechecked after fields).

New features and updates:

• Proof irrelevant \Prop.
• Right operator sections.
• New function and \case forms: \sfunc and \scase.
• Improved error messages.

First stable version