Twelf User's Guide
Version 1.2
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 Modes
6.1 Short Mode Declaration
6.2 Full Mode Declaration
6.3 Mode Checking
7 Termination
7.1 Termination Declaration
7.2 Subterm Ordering
7.3 Lexicographic Orders
7.4 Simultaneous Orders
7.5 Mutual Recursion
8 Theorem Prover
8.1 Theorem Declaration
8.2 Sample Theorems
8.3 Proof Steps
8.4 Search Strategies
8.5 Proof Realizations
9 ML Interface
9.1 Configurations
9.2 Loading Files
9.3 Environment Parameters
9.4 Timing Statistics
9.5 Twelf Signature
10 Twelf Server
10.1 Server Types
10.2 Server Commands
11 Emacs Interface
11.1 Twelf Mode
11.2 Editing Commands
11.3 Type Checking Commands
11.4 Error Tracking
11.5 Server State
11.6 Info File
11.7 Tags Files
11.8 Twelf Timers
11.9 Twelf-SML Mode
11.10 Emacs Variables
11.11 Syntax Highlighting
11.12 Emacs Initialization
11.13 Command Summary
12 Installation
13 Examples
Index
This document was generated on 18 November 1998 using the
texi2html
translator version 1.52.