TPSFLAG : ARGTYPE

TPSFLAG is an argument type.
A global flag or parameter.
Currently any of:
Top Levels: MT-DUPS-PER-QUANT PROOFW-ACTIVE PROOFW-ACTIVE+NOS PROOFW-ACTIVE+NOS-HEIGHT PROOFW-ACTIVE+NOS-WIDTH PROOFW-ACTIVE-HEIGHT PROOFW-ACTIVE-WIDTH PROOFW-ALL PROOFW-ALL-HEIGHT PROOFW-ALL-WIDTH
Style: STYLE
Review: ALPHA-LOWER-FLAG LAST-MODE-NAME
Modes: SUPPRESS-FLAGS SUPPRESS-FLAGS-LIST
Help: SHOW-ALL-PACKAGES
Starting and Finishing: COMPLETION-OPTIONS HISTORY-SIZE
OTL Object: AUTO-GENERATE-HYPS CLEANUP-RULEC CLEANUP-SAME DEFAULT-WFFEQ PRINT-DOTS PRINTLINEFLAG SHORT-HELP
Printing: PRINT-COMBINED-EGENS PRINT-COMBINED-UGENS PRINT-COMBINED-UIS PRINT-UNTIL-UI-OR-EGEN
Printing: ALLSCOPEFLAG ATOMVALFLAG BLANK-LINES-INSERTED CHARSIZE DISPLAYWFF ELIM-DEFNS FILLINEFLAG FIRST-ORDER-PRINT-MODE FLUSHLEFTFLAG LEFTMARGIN LOCALLEFTFLAG PPWFFLAG PRINTDEPTH PRINTTYPES PRINTTYPES-ALL RETAIN-INITIAL-TYPE RIGHTMARGIN SCOPE SLIDES-PREAMBLE USE-DOT USE-INTERNAL-PRINT-MODE
Internal for Printing: INFIX-NOTATION
TeX: IN-TEX-MATH-MODE LATEX-EMULATION PAGELENGTH TEX-MIMIC-SCRIBE
X Windows: USE-WINDOW-STYLE WINDOW-STYLE
Weak Labels: PRINT-WEAK
Flavors of Labels: MAKE-WFFOPS-LABELS META-LABEL-NAME PRINT-META
Saving Work: SAVE-INTERVAL SAVE-WORK-ON-START-UP SAVE-WORK-P
Recording: PRINTEDTFILE PRINTEDTFLAG PRINTEDTFLAG-SLIDES PRINTEDTOPS PRINTMATEFILE PRINTMATEFLAG PRINTMATEFLAG-SLIDES PRINTMATEOPS
Printing Proofs into Files: LATEX-POSTAMBLE LATEX-PREAMBLE SCRIBE-LINE-WIDTH SCRIBE-POSTAMBLE SCRIBE-PREAMBLE TEX-1-POSTAMBLE TEX-1-PREAMBLE TEX-LINE-WIDTH TEX-POSTAMBLE TEX-PREAMBLE TPSTEX VPDTEX
Proof Outline: PRINT-COMMENTS SLIDES-TURNSTILE-INDENT SLIDES-TURNSTYLE-INDENT SUPPORT-NUMBERS TURNSTILE-INDENT TURNSTILE-INDENT-AUTO TURNSTYLE-INDENT TURNSTYLE-INDENT-AUTO
Expansion Trees: ADD-TRUTH DUPLICATION-STRATEGY DUPLICATION-STRATEGY-PFD ECONJ-NAME EDISJ-NAME EMPTY-DUP-INFO-NAME EPROOF-NAME EXPANSION-NAME FALSE-NAME IMP-NAME INITIAL-BKTRACK-LIMIT LEAF-NAME MATING-NAME MATINGSTREE-NAME MIN-QUANTIFIER-SCOPE NEG-NAME PRINT-DEEP PRINT-NODENAMES RENUMBER-LEAVES REWRITE-DEFNS REWRITE-NAME SELECTION-NAME SHOW-SKOLEM SKOLEM-DEFAULT SKOLEM-SELECTION-NAME TRUE-NAME TRUTHVALUES-HACK
Mtree Operations: DEFAULT-OB MT-DEFAULT-OB-MATE
Mtree Auto: MT-SUBSUMPTION-CHECK MT94-12-TRIGGER MTREE-FILTER-DUPS MTREE-STOP-IMMEDIATELY TAG-CONN-FN TAG-MATING-FN
Mating search: DEFAULT-EXPAND DEFAULT-MATE DEFAULT-MS INTERRUPT-ENABLE MATING-VERBOSE MONITORFLAG NEW-MATING-AFTER-DUP QUERY-USER REC-MS-FILE REC-MS-FILENAME USE-DIY USE-FAST-PROP-SEARCH
MS88 search procedure: ADDED-CONN-ENABLED CONSIDERED-CONN-ENABLED DUP-ALLOWED DUPE-ENABLED DUPE-VAR-ENABLED EXCLUDING-GC-TIME FIRST-ORDER-MODE-MS INCOMP-MATING-ENABLED MATE-FFPAIR MATE-SUBSUMED-TEST-ENABLED MATE-SUBSUMED-TRUE-ENABLED MATING-CHANGED-ENABLED MS-INIT-PATH MS-SPLIT OCCURS-CHECK PRIM-QUANTIFIER PRIMSUB-ENABLED PROP-STRATEGY REMOVED-CONN-ENABLED SEARCH-COMPLETE-PATHS START-TIME-ENABLED STOP-TIME-ENABLED TIMING-NAMED UNIF-SUBSUMED-TEST-ENABLED UNIF-SUBSUMED-TRUE-ENABLED
MS89 search procedure: MAX-SEARCH-LIMIT RANK-EPROOF-FN SEARCH-TIME-LIMIT
MS90-3 search procedure: MAX-MATES MIN-QUANT-ETREE MS90-3-DUP-STRATEGY NUM-FRPAIRS PRINT-MATING-COUNTER SHOW-TIME
MS91-6 and MS91-7 search procedures: MS91-INTERLEAVE MS91-PREFER-SMALLER MS91-TIME-BY-VPATHS MS91-WEIGHT-LIMIT-RANGE NEW-OPTION-SET-LIMIT OPTIONS-GENERATE-ARG OPTIONS-GENERATE-FN OPTIONS-GENERATE-UPDATE OPTIONS-VERBOSE PENALTY-FOR-EACH-PRIMSUB PENALTY-FOR-MULTIPLE-PRIMSUBS PENALTY-FOR-MULTIPLE-SUBS PENALTY-FOR-ORDINARY-DUP RECONSIDER-FN WEIGHT-A-COEFFICIENT WEIGHT-A-FN WEIGHT-B-COEFFICIENT WEIGHT-B-FN WEIGHT-C-COEFFICIENT WEIGHT-C-FN
MS98-1 search procedure: BREAK-AT-QUANTIFIERS FF-DELAY HPATH-THRESHOLD MAXIMIZE-FIRST MS98-BASE-PRIM MS98-DUP-BELOW-PRIMSUBS MS98-DUP-PRIMSUBS MS98-FIRST-FRAGMENT MS98-FORCE-H-O MS98-FRAGMENT-ORDER MS98-INIT MS98-LOW-MEMORY MS98-MAX-COMPONENTS MS98-MAX-PRIMS MS98-MEASURE MS98-MERGE-DAGS MS98-MINIMALITY-CHECK MS98-NUM-OF-DUPS MS98-PRIMSUB-COUNT MS98-REW-PRIMSUBS MS98-REWRITE-DEPTH MS98-REWRITE-MODEL MS98-REWRITE-PRUNE MS98-REWRITE-SIZE MS98-REWRITE-UNIF MS98-REWRITES MS98-UNIF-HACK MS98-UNIF-HACK2 MS98-VALID-PAIR MS98-VARIABLE-ORDER MS98-VERBOSE
Proof Translation: ETREE-NAT-VERBOSE MERGE-MINIMIZE-MATING NATREE-DEBUG REMOVE-LEIBNIZ
Unification: APPLY-MATCH COUNTSUBS-FIRST DNEG-IMITATION ETA-RULE IMITATION-FIRST LEIBNIZ-SUB-CHECK MAX-DUP-PATHS MAX-SEARCH-DEPTH MAX-UTREE-DEPTH MIN-QUICK-DEPTH MS-DIR MS90-3-QUICK PRUNING REDUCE-DOUBLE-NEG RIGID-PATH-CK STOP-AT-TSN SUBSUMPTION-CHECK SUBSUMPTION-DEPTH SUBSUMPTION-NODES TOTAL-NUM-OF-DUPS UNI-SEARCH-HEURISTIC UNIF-COUNTER UNIF-COUNTER-OUTPUT UNIF-TRIGGER UNIFY-VERBOSE
Tactics: DEFAULT-TACTIC TACMODE TACTIC-VERBOSE TACUSE
suggestions: GO-INSTRUCTIONS QUIETLY-USE-DEFAULTS RESOLVE-CONFLICT
Searchlists: TEST-EASIER-IF-HIGH TEST-EASIER-IF-LOW TEST-EASIER-IF-NIL TEST-EASIER-IF-T TEST-FASTER-IF-HIGH TEST-FASTER-IF-LOW TEST-FASTER-IF-NIL TEST-FASTER-IF-T TEST-FIX-UNIF-DEPTHS TEST-INCREASE-TIME TEST-INITIAL-TIME-LIMIT TEST-MAX-SEARCH-VALUES TEST-NEXT-SEARCH-FN TEST-REDUCE-TIME TEST-VERBOSE TESTWIN-HEIGHT TESTWIN-WIDTH
Vpforms: LIT-NAME ORDER-COMPONENTS PRINT-LIT-NAME PRINTVPDFLAG TEXFORMAT VPD-BRIEF VPD-FILENAME VPD-LIT-NAME VPD-PTYPES VPD-STYLE VPD-VPFPAGE VPFORM-LABELS VPFORM-TEX-MAGNIFICATION VPFORM-TEX-NEST VPFORM-TEX-PREAMBLE VPW-HEIGHT VPW-WIDTH
Wff Editor: EDPPWFFLAG EDPRINTDEPTH EDWIN-CURRENT EDWIN-CURRENT-HEIGHT EDWIN-CURRENT-WIDTH EDWIN-TOP EDWIN-TOP-HEIGHT EDWIN-TOP-WIDTH EDWIN-VPFORM EDWIN-VPFORM-HEIGHT EDWIN-VPFORM-WIDTH
wff Primitives: META-BDVAR-NAME META-VAR-NAME REN-VAR-FN RENAME-ALL-BD-VARS
Wff Parsing: BASE-TYPE FIRST-ORDER-MODE-PARSE LOWERCASERAISE TYPE-IOTA-MODE UNTYPED-LAMBDA-CALCULUS
Basic Abbreviations: REWRITE-EQUALITIES
Lambda-Calculus: LAMBDA-CONV
Primitive Substitutions: MAX-PRIM-DEPTH MAX-PRIM-LITS MIN-PRIM-DEPTH MIN-PRIM-LITS NEG-PRIM-SUB PR97C-MAX-ABBREVS PR97C-PRENEX PRIM-BDTYPES PRIM-BDTYPES-AUTO PRIM-PREFIX PRIMSUB-METHOD
Miscellaneous: REWRITE-EQUIVS
RuleP: RULEP-MAINFN RULEP-WFFEQ
Skolemizing: NAME-SKOLEM-FN
Quantifiers: UI-HERBRAND-LIMIT
Auxiliary: USE-RULEP USE-SYMSIMP
Events: ADVICE-ASKED-ENABLED ADVICE-FILE COMMAND-ENABLED COMMAND-FILE DONE-EXC-ENABLED ERROR-ENABLED ERROR-FILE EVENT-CYCLE EVENTS-ENABLED INPUT-ERROR-ENABLED INPUT-ERROR-FILE PROOF-ACTION-ENABLED PROOF-FILE QUIET-EVENTS RULE-ERROR-ENABLED RULE-ERROR-FILE SCORE-FILE
Grader: CAL-PERCENTAGE COURSE-NAME DEFAULT-PENALTY-FN DROP-MIN DUE-DATE-FLAG ETPS-FILE GRADE-DIR GRADE-FILE LETTER-GRADE-FILE LETTER-GRADE-FLAG NEW-ITEM OLD-GRADE-FILE OLD-TOTALS-GRADE-FILE PATCH-FILE PRINT-N-DIGITS STATISTICAL-OPTIONS TOTALS-GRADE-FILE
Maintenance: COMPILED-EXTENSION EXPERTFLAG INIT-DIALOGUE INIT-DIALOGUE-FN LISP-IMPLEMENTATION-TYPE LOAD-WARN-P MACHINE-INSTANCE MACHINE-TYPE NEWS-DIR READ-LLOAD-SOURCES-P SAVE-FILE SHORT-SITE-NAME SOURCE-EXTENSION SOURCE-PATH TEST-MODIFY TEST-THEOREMS
Rules object: BUILD-MATCH HLINE-JUSTIFICATION TREAT-HLINES-AS-DLINES
Unclassified: MAX-SUBSTS-PROJ MAX-SUBSTS-PROJ-TOTAL MAX-SUBSTS-QUICK MAX-SUBSTS-VAR NUM-OF-DUPS PRIMSUB-VAR-SELECT
Library: ADD-SUBDIRECTORIES BACKUP-LIB-DIR DEFAULT-LIB-DIR DEFAULT-LIBFILE-TYPE DEFAULT-LIBINDEX-TYPE LIB-BESTMODE-FILE LIB-KEYWORD-FILE LIB-MASTERINDEX-FILE RECORDFLAGS REMOVE-TRAILING-DIR SHOW-ALL-LIBOBJECTS
Bugs: DEFAULT-BUG-DIR USE-DEFAULT-BUG-DIR

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage