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
• 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 features in the following:

• Univalent features similar to Cubical Agda, redtt, and Arend,
• Overlapping and order-independent pattern matching,
• Practical functional programming features similar to Haskell and Idris.