## Arend 1.10.0 released

Language updates:

Language updates:

- Bug fixes and minor improvements

Plugin updates:

- Keyword documentation
- Improved change signature refactoring
- Improved move refactoring
- Improved parameter hints
- Improved REPL, completion, auto-import, and import optimization
- Improved settings synchronization
- Latex in documentation strings
- Class diagrams
- Quick braces switch intention

arend-lib:

- Tactics:
- assumption meta
- in meta
- defaultImpl meta

- Sets and logic:
- Pigeonhole principle
- Kuratowski-finite sets
- “The following are equivalent” proofs
- Countable sets
- Subset operations
- Simplified syntax for quantifiers
- Partial elements

- Algebra:
- Graded rings, homogeneous ideals, homogeneous localizations, Proj construction
- Lagrange’s theorem
- Dimension of a ring, a characterization of zero-dimensional rings, zero-dimensional local rings, and von Neumann regular rings
- A characterization of Smith rings
- PIDs are Smith domains
- PIDs are 1-dimensional
- Euclidean domains are PIDs
- Polynomial division
- Matrix ring
- Various definitions of determinant and a proof that they are equivalent
- Various properties of determinant
- Symmetric group, its cardinality, sign homomorphism
- Characteristic polynomial of a matrix and a proof that eigenvalues are its roots
- Integral elements and extensions, a characterization of finitely generated integral extensions
- Monoid rings and multivariate polynomials
- Valuation rings
- Factor rings and factor fields
- Nakayama’s lemma
- The minimal polynomial of an element of a ring extension
- A proof that a finitely generated extension is integral if and only if it is zero-dimensional
- The Chinese remainder theorem
- Dimension of a finite free module
- Independent sets, bases, and their various properties
- The image and the kernel of a linear map between finite modules over a Smith domain are finite
- Linear dependency is decidable in a finite module over a Smith domain
- Splitting fields of polynomials over countable fields
- Rank of a matrix over a Smith domain
- Surjective linear endomaps on a finitely generated module are bijective
- Cayley-Hamilton theorem
- Direct limits of algebraic structures over semilattices
- Algebraically closed fields and the algebraic closure of a countable field
- The absolute value for linearly ordered abelian groups
- Group actions
- First isomorphism theorem

- Topology:
- Cover spaces
- Completion of cover spaces
- Uniform spaces and their completion
- Metric spaces and their completion
- Equivalence between appropriate subcategories of complete cover spaces and regular locales
- Topological abeliean groups and their completion
- Normed abelian groups, normed rings, Banach spaces
- Products of topological spaces, cover spaces, uniform spaces, and topological abelian groups
- Normed abelian group of real numbers
- Compact spaces and a characteriization of cover maps
- Cover space structure on directed sets

- Analysis:
- Limit of a function on a directed set
- Uniform convergence
- Series and various convergence tests
- Power series and their radius of convergence

- Real and complex numbers:
- The field of real numbers
- The field of complex numbers
- The exponential function on real numbers

- Categories:

Language updates:

Language updates:

Language updates:

There is a new tutorial on interactive theorem proving with IntelliJ Arend. Check it out to learn about the features of IntelliJ Arend that speed-up theorem...

Language updates:

Language updates: Built-in finite types \default implementations \coerce to function types \coerce for fields and constructors \have declaration ...

Language updates: String literals, which can be used in meta code Meta resolvers, which can be used to modify the scoping rules for meta definitions \...

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. ...

The second part of our tutorial is ready.

We implemented language extensions. This can be used to implement custom operations on the abstract syntax tree which are not supported by the language. They...

We finished the first part of our new tutorial. It covers all the basic constructions of Arend. It does not mention anything related to homotopy theory. This...

We implemented a few features related to classes and pattern matching. One of these features is pattern matching on idp : a = a, which can be used instead of...

Arend now has proof irrelevant universe of proposition and the plugin can run the typechecker automatically in background.

The first version of Arend is released!