Referencemanual

LANGUAGE REFERENCE MANUAL

objects and types

giving names

 Things which we can declare
 functions, datatypes, records

Functions - Bengt

 Declaration, Syntax, Use

Datatypes - Peter

 Declaration, Syntax, Use

Pattern match - Pierre

 declaration of functions from a datatype

Records - Yoshiki

 Declaration, Syntax, Use
 can be regarded as datatypes with one constructor!

Modules

 Declaration, Syntax, Use

Postulates - introduction of constants Local Definitions - Anna Lexical matters Implicit arguments - Thierry Syntactic sugars

 Mixfix syntax - Thierry
 With notation - Thierry

EXAMPLES

 Small nice examples
 Examples showing the use of dependent types

USING AGDA

 How to download/install the system / DONE
 Emacs interface / Command line invocation
 Foreign Function Interface
 Plug-in
 Unicode / How to input special characters
 Literate Agda
 Compiler

THEORY

 Termination checker
 Type checker (informative description of operational semantics, conversion)

LIBRARY

Structured description of libraries