Agda User Manual
User Manual:
Open the PDF directly: View PDF
Page Count: 157 [warning: Documents this large are best viewed by clicking the View PDF Link!]
- Overview
- Getting Started
- Language Reference
- Abstract definitions
- Built-ins
- Coinduction
- Copatterns
- Core language
- Cubical Type Theory in Agda
- Data Types
- Foreign Function Interface
- Function Definitions
- Function Types
- Implicit Arguments
- Instance Arguments
- Irrelevance
- Lambda Abstraction
- Local Definitions: let and where
- Lexical Structure
- Literal Overloading
- Mixfix Operators
- Module System
- Mutual Recursion
- Pattern Synonyms
- Positivity Checking
- Postulates
- Pragmas
- Record Types
- Reflection
- Rewriting
- Safe Agda
- Sized Types
- Syntactic Sugar
- Syntax Declarations
- Telescopes
- Termination Checking
- Universe Levels
- With-Abstraction
- Without K
- Tools
- Contribute
- The Agda License
- The Agda Team
- Indices and tables
- Bibliography