Agda Tutorial

General Information

import Motivation

import Installation

import Emacs_Usage

Sets

import Modules.Basic
import Sets.Enumerated
import Sets.Recursive
import Constants
import Syntax.Decimal_Naturals
import Syntax.Infix
import Sets.Mutual
import Sets.Parametric

import Sets.Indexed
import Term_Inference
import Sets.Propositions
import Sets.Parameters_vs_Indices

Functions

import Functions.Cases
import Functions.Recursive
import Functions.Polymorphic
import Functions.Functions_vs_Sets
import Functions.Large

import Functions.Dependent
import Functions.Universal_Quantification
import Functions.Equality_Proofs
import Sets.With_Functions

import Sets.Sigma

import Functions.Views
import Functions.Views.Decidability

Modules and records

import Modules.Advanced
import Modules.Parameterised
import Modules.Data
import Modules.Imports
import Sets.Records
import Modules.Records

Applications

import Application.Algebra

Other material

• Presentation for mathematicians

import Modules.Standard_Libraries

import Further_Reading

import About