Contents

• Contents
• Introduction
• Customising the Library
  • Universes
  • Equality
• Conventions
• Providing logic and equality
  • Logic
  • Equality
    • Martin-Löf's Inductive Equality
    • Leibniz Equality
    • Paulin-Mohring's Inductive Equality
    • Altenkirch-Streicher Elimination Rule
    • Theorems about Equality
  • Setoids
• The Empty Type
• The Unit Type
• The Booleans
  • Boolean Definition
  • Boolean Functions
  • Boolean Theorems
• Product Types
• Sum Types
• Inductive Sigma
• The Natural Numbers
  • Natural Numbers: Basic Definitions
  • Iteration Principles
  • Induction Principles
  • Theorems about Successor
  • Theorems about Minus
  • Theorems about Plus
  • Theorems about multiplication
  • Square Roots
  • Order relations
    • Propositional Inequality
    • Propositional Strict Inequality
    • Propositional Relations
    • Boolean-valued Relations
    • All order relations
  • The predicate Even
  • Max and Min
  • Division
  • Exponentiation
• List
  • List Definitions
  • List Basics
  • List functions with booleans
  • Partial List functions
  • Length-like list functions
  • Other list functions
  • Lists and products
  • The Relation Adjoin
  • Membership
  • Distinctness
  • Permutation
  • Sorted Lists
• Finite Sets
• Vectors
  • Vector Definitions
  • Vector Basics
• Quotient Types
• Relations
  • Definitions
  • Relation closures
• Set theory
• The Integers
  • Extra lemmas for integers
  • The Integers--Definitions
  • Basic Lemmas
  • Some theorems about Modulo
  • Boolean valued functions on the integers
  • Propositional relations on integers
  • Max and min on integers
• Specification and development of functional programs
• Pure Martin Löf type theory
  • Basic properties
  • Natural Numbers: Basic theorems
• References