ARGTYPE : argument type

Review

• dev-style
• fsym
• subject
• subjectlist
• symbollist
• tps-mode

Flags

• flag-and-val
• fv-list
• tpsflag

Help

• help*-list
• symbol-or-integer-list

Collecting Help

• context
• contextlist
• dev-stylelist
• tpscat
• tpscatlist

Starting and Finishing

• dirspec
• dirspeclist
• filespec

Printing

• print-function
• print-function-list

Printing

• ignore
• indentation

Saving Wffs

• weak-label
• weak-label-list

Proof Outline

• existing-line
• existing-linelist
• justification
• line
• line-range
• line-range-list
• linelist
• lvarconst
• occlist
• pline
• rline
• rlinelist

Expansion Trees

• boolean-or-abbrevlist
• etree
• rewrite-defns-list

Mtree Printing

• matingstree
• obdefault

Mating search

• gwff0
• gwff0-or-eproof
• gwff0-or-label-or-eproof
• leaftype
• mate-command
• matingpair
• matingpairlist
• mt-subsumption
• querytype
• searchtype

Unification

• verbose

Tactics

• tactic-exp
• tactic-mode
• tactic-use

suggestions

• exec-form
• go-instruct

Searchlists

• anything-list

Vpforms

• jform
• vpformat
• vpstyle

Theorems

• book-theorem
• exercise
• lib-theorem
• practice
• test-problem
• theorem
• theoremlist

Wff Editor

• ed-command
• msglist
• msglistlist

Wff Types

• gvar
• gvarlist
• gwff
• gwff-ill
• gwff0-or-label
• gwffalist
• gwfflist
• gwffpair
• gwffpairlist
• occ-list
• ordercom
• typealist
• typesym
• typesym-cons
• typesym-nil
• typesymlist
• typesymlist-nil
• wffset

Rewriting commands

• rrule
• rrulelist
• theory

Substitution

• repsym

Basic Abbreviations

• rewrite-defns

RuleP

• rulep-mainfn-type

Skolemizing

• subst-alist
• subst-pair

Grader

• consp1
• function

Maintenance

• symbolpair
• symbolpairlist

Basics

• anything
• boolean
• integer+
• integer+-or-infinity
• null-or-integer
• null-or-posinteger
• posinteger
• posinteger-or-infinity
• posintegerlist
• posnumber
• string
• symbol
• symbol-or-integer
• yesno

Modules

• modulelist
• tps-module

Rules Module

• rule

Lisp packages

• lisp-package
• lisp-package-list

Library

• filespeclist
• gwff-prop
• gwff-prop-list
• lib-argtype
• lib-argtype-list
• lib-argtype-or-nil
• stringlist
• stringlistlist
• tpsflaglist

Best modes

• short-date

TPS documentation homepage

TPS homepage