3. Language Elements

The language elements are highly mutully recursive. E.g. definitions contain expressions and expressions can contain local definitions. Therefore there is no natural order to present the language elements and we present them in alphabetic order.

However the most important language concepts are:

• Projects

• Packages

• Modules

• Inductive Types

• Functions

• Pattern Match

Alphabetic list:

• 3.1. Abstract Data Types
• 3.2. Do Notation
• 3.3. Functions
• 3.4. Inductive Types
• 3.5. Implicit Arguments
• 3.6. Inspect Expression
• 3.7. Lexical Structure
• 3.8. Local Definitions
• 3.9. Modules
• 3.10. Namespaces
• 3.11. Packages
• 3.12. Pattern Match
• 3.13. Precedence and Associativity
• 3.14. Projects
• 3.15. Records
• 3.16. Sections
• 3.17. Style and Conventions
• 3.18. Telescopes / Formal Arguments
• 3.19. Types
• 3.20. Universes / Sorts