Next:
Contents
The LEGO library - Version 1.3
LEGO Team
<lego@dcs.ed.ac.uk>
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
Bibliography
About this document ...
Lego
1998-06-15