欢迎阅读 Agda 文档！

• 概览
• 起步
  • Agda 是什么？
  • 前提需求
  • 安装
  • Agda 的「Hello world」
  • 快速指南：Agda 代码的编辑、类型检查与编译
  • 教程列表
• Language Reference
  • Abstract definitions
  • Built-ins
  • Coinduction
  • Copatterns
  • Core language
  • Cubical
  • Data Types
  • Foreign Function Interface
  • Function Definitions
  • Function Types
  • Generalization of Declared Variables
  • 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
  • Prop
  • Record Types
  • Reflection
  • Rewriting
  • Safe Agda
  • Sized Types
  • Syntactic Sugar
  • Syntax Declarations
  • Telescopes
  • Termination Checking
  • Universe Levels
  • With-Abstraction
  • Without K
• Tools
  • Automatic Proof Search (Auto)
  • Command-line options
  • Compilers
  • Emacs Mode
  • Literate Programming
  • Generating HTML
  • Generating LaTeX
  • Library Management
• Contribute
  • Documentation
• The Agda Team and License

索引和列表

• 索引
• 搜索页面