Agda Tutorial

General Information

import Motivation

import Installation

import Emacs_Usage
import Symbols

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.Negation
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
import Revise.Reflection

Coinduction

import Revise.Coinduction
import Revise.IO
import Revise.InfIO

Other material

• Presentation for mathematicians

import Modules.Standard_Libraries

import Further_Reading

import About