Twelf User's Guide

Version 1.4

• 1 Introduction
  • 1.1 New Features
  • 1.2 Quick Start
• 2 Lexical Conventions
  • 2.1 Reserved Characters
  • 2.2 Identifiers
• 3 Syntax
  • 3.1 Grammar
  • 3.2 Constructor Declaration
  • 3.3 Definitions
  • 3.4 Operator Declaration
  • 3.5 Name Preferences
  • 3.6 Sample Signature
• 4 Term Reconstruction
  • 4.1 Implicit Quantifiers
  • 4.2 Implicit Arguments
  • 4.3 Strict Occurrences
  • 4.4 Strict Definitions
  • 4.5 Type Ascription
  • 4.6 Error Messages
  • 4.7 Tracing Reconstruction
• 5 Logic Programming
  • 5.1 Query Declaration
  • 5.2 Solve Declaration
  • 5.3 Interactive Queries
  • 5.4 Sample Trace
  • 5.5 Operational Semantics
  • 5.6 Sample Program
  • 5.7 Clause Definitions
  • 5.8 Deterministic Type Families
  • 5.9 Tabled Logic Programming
• 6 Constraint Domains
  • 6.1 Installing an Extension
  • 6.2 Equalities over Rational Numbers
  • 6.3 Inequalities over Rational Numbers
  • 6.4 Integer Constraints
  • 6.5 Equalities over Strings
  • 6.6 32-bit Integers
  • 6.7 Sample Constraint Programs
  • 6.8 Restrictions and Caveats
• 7 Modes
  • 7.1 Short Mode Declaration
  • 7.2 Full Mode Declaration
  • 7.3 Mode Checking
• 8 Termination
  • 8.1 Termination Declaration
  • 8.2 Reduction Declaration
  • 8.3 Subterm Ordering
  • 8.4 Lexicographic Orders
  • 8.5 Simultaneous Orders
  • 8.6 Mutual Recursion
• 9 Coverage
  • 9.1 Regular Worlds
  • 9.2 Input Coverage
  • 9.3 Totality
  • 9.4 Subordination
• 10 Theorem Prover
  • 10.1 Theorem Declaration
  • 10.2 Sample Theorems
  • 10.3 Proof Steps
  • 10.4 Search Strategies
  • 10.5 Proof Realizations
• 11 ML Interface
  • 11.1 Configurations
  • 11.2 Loading Files
  • 11.3 Environment Parameters
  • 11.4 Signature Printing
  • 11.5 Tracing and Breakpoints
  • 11.6 Timing Statistics
  • 11.7 Twelf Signature
• 12 Twelf Server
  • 12.1 Server Types
  • 12.2 Server Commands
• 13 Emacs Interface
  • 13.1 Twelf Mode
  • 13.2 Editing Commands
  • 13.3 Type Checking Commands
  • 13.4 Printing Commands
  • 13.5 Tracing Commands
  • 13.6 Error Tracking
  • 13.7 Server State
  • 13.8 Info File
  • 13.9 Tags Files
  • 13.10 Twelf Timers
  • 13.11 Twelf-SML Mode
  • 13.12 Emacs Variables
  • 13.13 Syntax Highlighting
  • 13.14 Emacs Initialization
  • 13.15 Command Summary
• 14 Installation
• 15 Examples
• 16 History
• Index

This document was generated on 27 December 2002 using the texi2html translator version 1.52.