Summary

• Table of Contents
• Abstract
• Introduction
• Get and Use the Compiler
• Language Concepts
  • Module and Package System
  • Conventions
  • Builtin Types and Functions
    • BOOLEAN and ANY
    • PREDICATE
    • FUNCTION
    • TUPLE
    • LIST
  • Function Definitions
• Classes
  • Inductive Classes
    • Declaration
    • Pattern Matching
    • Equality
    • Inheritance from ANY
    • Induction Law
    • Induction Proofs
    • More on Induction Proofs
    • Generalizing the Induction Goal
  • Abstract Classes
    • Declaration
    • Inheritance
    • Function Redefinitions
    • Rename
  • Pseudoinductive Classes
    • Motivation
    • Machine Number
    • Induction Law
    • Recognizer
    • Projector
    • Recursion
    • History
• Inductive Sets and Relations
  • Inductive Definition
  • Form of the Rules
  • Using the Rules
  • Induction Proof
  • Induction Principle
  • More on Induction
• Theorems
• Proof Engine
• Bibliography