# The Aya Prover

- Installation Guide
- Tutorial for functional programmers (such as ML, Haskell, or Idris users)
- Tutorial for dependent types or theorem prover users
- Tutorial for VSCode extension
- Tutorial for the fake literate mode

Aya is a programming language *and* an interactive proof assistant designed for type-directed programming *and* formalizing math.

The type system of Aya has the following highlights:

- Set-level cubical features so
`funExt`

and quotients are available without axioms (like Agda, redtt, and Arend but not higher-dimensional), - Overlapping and order-independent pattern matching makes simple functions compute better,
- Practical functional programming features similar to Haskell and Idris: dependent pattern matching, typed holes, enchanted synthesis of implicit arguments.

The implementation of the Aya compiler has the following highlights:

- Efficient type checking by JIT-compiling well-typed definitions to JVM higher-order abstract syntax, so substitution does not traverse terms,
- Convenient interactive tools such as a language server for VSCode, a REPL, and hyperlinked document generation (demo),
- Pre-compiled binary release.