Twelf User's Guide
Version 1.3
Frank Pfenning and Carsten Schuermann
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
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
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 String
6.6 Sample Constraint Programs
6.7 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 Theorem Prover
9.1 Theorem Declaration
9.2 Sample Theorems
9.3 Proof Steps
9.4 Search Strategies
9.5 Proof Realizations
10 ML Interface
10.1 Configurations
10.2 Loading Files
10.3 Environment Parameters
10.4 Signature Printing
10.5 Tracing and Breakpoints
10.6 Timing Statistics
10.7 Twelf Signature
11 Twelf Server
11.1 Server Types
11.2 Server Commands
12 Emacs Interface
12.1 Twelf Mode
12.2 Editing Commands
12.3 Type Checking Commands
12.4 Printing Commands
12.5 Tracing Commands
12.6 Error Tracking
12.7 Server State
12.8 Info File
12.9 Tags Files
12.10 Twelf Timers
12.11 Twelf-SML Mode
12.12 Emacs Variables
12.13 Syntax Highlighting
12.14 Emacs Initialization
12.15 Command Summary
13 Installation
14 Examples
15 History
Index
This document was generated on 16 October 2000 using the
texi2html
translator version 1.52.