[
Top
]
[
Contents
]
[
Index
]
[
?
]
Table of Contents
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. Module System
5.1 Signature Declaration
5.2 Structure Declaration
5.3 View Declaration
5.4 Include Declaration
5.5 Morphisms
5.6 Open Declaration
6. Logic Programming
6.1 Query Declaration
6.2 Solve Declaration
6.3 Interactive Queries
6.4 Sample Trace
6.5 Operational Semantics
6.6 Sample Program
6.7 Clause Definitions
6.8 Deterministic Type Families
6.9 Tabled Logic Programming
7. Constraint Domains
7.1 Installing an Extension
7.2 Equalities over Rational Numbers
7.3 Inequalities over Rational Numbers
7.4 Integer Constraints
7.5 Equalities over Strings
7.6 32-bit Integers
7.7 Sample Constraint Programs
7.8 Restrictions and Caveats
8. Modes
8.1 Short Mode Declaration
8.2 Full Mode Declaration
8.3 Mode Checking
9. Termination
9.1 Termination Declaration
9.2 Reduction Declaration
9.3 Subterm Ordering
9.4 Lexicographic Orders
9.5 Simultaneous Orders
9.6 Mutual Recursion
10. Coverage
10.1 Regular Worlds
10.2 Input Coverage
10.3 Totality
10.4 Subordination
11. Theorem Prover
11.1 Theorem Declaration
11.2 Sample Theorems
11.3 Proof Steps
11.4 Search Strategies
11.5 Proof Realizations
12. ML Interface
12.1 Configurations
12.2 Loading Files
12.3 Environment Parameters
12.4 Signature Printing
12.5 Tracing and Breakpoints
12.6 Timing Statistics
12.7 Twelf Signature
13. Twelf Server
13.1 Server Types
13.2 Server Commands
14. Emacs Interface
14.1 Twelf Mode
14.2 Editing Commands
14.3 Type Checking Commands
14.4 Printing Commands
14.5 Tracing Commands
14.6 Error Tracking
14.7 Server State
14.8 Info File
14.9 Tags Files
14.10 Twelf Timers
14.11 Twelf-SML Mode
14.12 Emacs Variables
14.13 Syntax Highlighting
14.14 Emacs Initialization
14.15 Command Summary
15. Installation
16. Examples
17. History
Index
[
Top
]
[
Contents
]
[
Index
]
[
?
]
This document was generated by
Florian Rabe
on
April, 3 2009
using
texi2html 1.76
.