The Aya Prover
- Installation Guide
- Tutorial for Haskellers (should also work for Idris users)
- Tutorial for Dependent Type users
- Tutorial for the "extension type"
- Tutorial for VSCode extension
Aya is a programming language and an interactive proof assistant designed for type-directed programming and formalizing math.
The type system of Aya features in the following: