Getting Started

• What is Agda?
  • Dependent types
• Installation
  • Step 1: Install Agda
  • Step 2: Configure a text editor
  • Step 3: Install agda-stdlib (optional)
  • Step 4: Install ghc (optional)
• Troubleshooting
  • Windows invalid byte sequence
  • macOS notarization
  • Cabal issues
• ‘Hello world’ in Agda
  • Hello, Agda!
  • Hello, World!
• A Taste of Agda
  • Preliminaries
  • Programming With Dependent Types: Vectors
  • Agda as a Proof Assistant: Proving Associativity of Addition
  • Building an Executable Agda Program
  • Where to go from here?
• A List of Tutorials
  • Books on Agda
  • Tutorials and lecture notes
  • Videos on Agda
  • Courses using Agda
  • Miscellaneous