Twelf User's Guide

Version 1.2

• 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.