Bug fixes and minor improvements

• 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