Index (CZT to Z/EVES 1.6-SNAPSHOT API)

A B C D E F G H I L M N O P Q R S T U V W X Z

A

ABILITY_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = Ability => label.getAbility();
addCommand(String, boolean, boolean) - Method in class net.sourceforge.czt.zeves.proof.ZEvesTactics.CommandSequence
addError(Position, SnapshotData) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Adds an error result (a Z/EVES error) for a certain position to the snapshot.
addGoalResult(Position, String, SnapshotData) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Adds a Z/EVES result for a proof script goal ("try-lemma") to the snapshot.
addParaResult(Position, int, SnapshotData) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Adds a Z/EVES result for a submitted paragraph (non-ProofScript) to the snapshot.
addProofResult(Position, String, int, SnapshotData) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Adds a Z/EVES result for a submitted proof command to the snapshot.
addServerListener(ZEvesServerListener) - Method in class net.sourceforge.czt.zeves.ZEvesServer
addSnapshotChangedListener(ISnapshotChangedListener) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot
APPL_EXPR_BAG_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
APPL_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} expression => getExpr(term.getLeftExpr()); {1} expression => getExpr(term.getRightExpr()); NOTE: Added parentheses on the argument, because it may bind stronger than the expression.
APPL_EXPR_SEQ_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} comma sep list of expressions from getExpr(ZUtils.getApplExprArguments(term).get(n));
AXIOMATIC_BOX_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = decl-part => getDeclPart(term.getZSchText().getZDeclList()); {3} = axiom-part => getAxiomPart(term.getSchText().getPred());

B

back() - Method in class net.sourceforge.czt.zeves.ZEvesApi
back(int) - Method in class net.sourceforge.czt.zeves.ZEvesApi
BasicZEvesTranslator - Class in net.sourceforge.czt.zeves.z
BasicZEvesTranslator() - Constructor for class net.sourceforge.czt.zeves.z.BasicZEvesTranslator: Creates a new instance of BasicZEvesTranslator
BIN_PRED_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = predicate => getPred(term.getLeftPred()); {1} = operator => getBinPredName(term); = "∧" | ∨" | "⇒" | "⇔" {2} = predicate => getPred(term.getRightPred()); Note: "∧" needs to be treated specially, as we want to consider labelled-predicates (i.e.
BIN_SCHEXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} expression => getExpr(term.getLeftExpr()); {1} sch-op-name => getSchExprOpName(term); {2} expression => getExpr(term.getRightExpr()); NOTE: All SchExpr2 patterns: CompExpr, PipeExpr, ProjExpr, AndExpr, OrExpr, ImpliesExpr, and IffExpr.
BIND_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} semi-colon sep list of bindings as NAME : EXPR ; NAME : EXPR ...
BINDSEL_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
BRANCH_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = var-name => getVarName(term.getZName()); {1} = expr => getExpr(term.getExpr());
build() - Method in class net.sourceforge.czt.zeves.snapshot.SnapshotData.Builder
Builder(Term) - Constructor for class net.sourceforge.czt.zeves.snapshot.SnapshotData.Builder

C

clear() - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Clears the data stored in Z/EVES snapshot (to be used with accompanying ZEvesApi.reset()).
close() - Method in class net.sourceforge.czt.zeves.ZEvesApi
close() - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
CommandSequence(int) - Constructor for class net.sourceforge.czt.zeves.proof.ZEvesTactics.CommandSequence
COMMENT_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
completeSection(Position, String, String) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Marks the section completed.
concat(Collection<?>, String) - Static method in class net.sourceforge.czt.zeves.response.ZEvesResponseUtil
COND_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} predicate => getPred(term.getPred()); {1} expression => getExpr(term.getLeftExpr()); {2} expression => getExpr(term.getRightExpr());
connect() - Method in class net.sourceforge.czt.zeves.ZEvesApi
connect() - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
connectRetry(int) - Method in class net.sourceforge.czt.zeves.ZEvesApi
createEndLoop(int, List<String>) - Static method in class net.sourceforge.czt.zeves.proof.ZEvesTactics.CommandSequence
createReader() - Static method in class net.sourceforge.czt.zeves.response.ZEvesResponseReader
createSingle(String) - Static method in class net.sourceforge.czt.zeves.proof.ZEvesTactics.CommandSequence
createZEvesIncompatibleExceptionMessage(String, Term) - Static method in exception net.sourceforge.czt.zeves.ZEvesIncompatibleASTException
CZT2ZEves - Class in net.sourceforge.czt.zeves
CZT2ZEves() - Constructor for class net.sourceforge.czt.zeves.CZT2ZEves: Creates a new instance of CZT2ZEves
CZT2ZEvesPrinter - Class in net.sourceforge.czt.zeves.z: This class converts CZT terms, more precisely Para, Expr, or Pred, to Z/EVES socket server XML API.
CZT2ZEvesPrinter(SectionInfo) - Constructor for class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter: Creates a new instance of ZPrinter

D

DEFAULT_ADDRESS - Static variable in class net.sourceforge.czt.zeves.CZT2ZEves
DEFAULT_AUTOFLUSH_ZEVES_OUT - Static variable in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
DEFAULT_PORT - Static variable in class net.sourceforge.czt.zeves.CZT2ZEves
DEFAULT_ZEVES_HOST_ADDRESS - Static variable in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
DEFAULT_ZEVES_SERVER_PORT - Static variable in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
disconnect() - Method in class net.sourceforge.czt.zeves.ZEvesApi

E

EQ_SIGN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
EQ_SUBST_APPL_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
equals(Object) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot.FileSection
escapeUnicode(String) - Static method in class net.sourceforge.czt.zeves.response.ZEvesResponseReader

F

fetchOpTable() - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
FileSection(String, String) - Constructor for class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot.FileSection
finalize() - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
format(String, Object...) - Method in class net.sourceforge.czt.zeves.z.BasicZEvesTranslator: Applies the format operation from the underlying MessageFormat object set to the last pattern.

G

GENERIC_BOX_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = generic formals => getGenFormals(term.getZName()); {3} = decl-part => getDeclPart(term.getZSchText().getZDeclList()); {4} = axiom-part => getAxiomPart(term.getSchText().getPred());
getAutoFlushZEvesOut() - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
getBackwardsProofIterator(ISnapshotEntry, boolean) - Static method in class net.sourceforge.czt.zeves.snapshot.SnapshotUtil
getBanner() - Static method in class net.sourceforge.czt.zeves.ZEves
getCommand() - Method in class net.sourceforge.czt.zeves.proof.ZEvesTactics.IgnorableCommand
getCommand() - Method in class net.sourceforge.czt.zeves.response.ZEvesOutput
getCommands() - Method in class net.sourceforge.czt.zeves.proof.ZEvesTactics.CommandSequence
getContent() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesBlurb
getContext() - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
getCurrentGoalName() - Method in class net.sourceforge.czt.zeves.ZEvesApi
getData() - Method in interface net.sourceforge.czt.zeves.snapshot.ISnapshotEntry
getDebugInfo() - Method in exception net.sourceforge.czt.zeves.ZEvesException
getEntries() - Method in class net.sourceforge.czt.zeves.snapshot.SnapshotChangedEvent
getEntries(String, Position) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Retrieves snapshot results for the given specification file and position in it.
getEntries() - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Retrieves all results currently stored in the snapshot, for all submitted sections.
getFilePath() - Method in interface net.sourceforge.czt.zeves.snapshot.ISnapshotEntry
getFilePath() - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot.FileSection
getFirstResult() - Method in class net.sourceforge.czt.zeves.response.ZEvesOutput
getForm() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesLetDef
getForm() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesOp
getForm() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesReplace
getForm() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesAbbrevDef
getForm() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesBranch
getForm() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesHorSchDef
getGenActInfo(List<?>) - Static method in class net.sourceforge.czt.zeves.response.form.ZEvesName
getGenActuals() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesName
getGenChar(List<ZEvesName>) - Static method in class net.sourceforge.czt.zeves.response.para.ZEvesAxDef
getGenFormalsInfo(List<ZEvesName>) - Static method in class net.sourceforge.czt.zeves.response.para.ZEvesAxDef
getGoalName() - Method in class net.sourceforge.czt.zeves.snapshot.SnapshotData
getGoalProofLength(String) - Method in class net.sourceforge.czt.zeves.ZEvesApi
getGoalProofStep(String, int) - Method in class net.sourceforge.czt.zeves.ZEvesApi
getGoalProvedState(String) - Method in class net.sourceforge.czt.zeves.ZEvesApi
getHistoryElement(int) - Method in class net.sourceforge.czt.zeves.ZEvesApi
getHistoryLength() - Method in class net.sourceforge.czt.zeves.ZEvesApi
getHost() - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
getHostInfo() - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
getIdent() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesName
getInfo(ZEvesAbbrevDef.AbbrevType) - Static method in enum net.sourceforge.czt.zeves.response.para.ZEvesAbbrevDef.AbbrevType
getInfo(ZEvesAbility) - Static method in enum net.sourceforge.czt.zeves.response.para.ZEvesAbility
getInfo(ZEvesUsage) - Static method in enum net.sourceforge.czt.zeves.response.para.ZEvesUsage
getInfo() - Method in class net.sourceforge.czt.zeves.response.ZEvesOutput
getItem() - Method in class net.sourceforge.czt.zeves.response.XmlAnyElementItem
getItems() - Method in class net.sourceforge.czt.zeves.response.XmlAnyElementList
getLastPositionOffset(String) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Retrieves the max offset in the snapshot for the given file.
getLoopCount() - Method in class net.sourceforge.czt.zeves.proof.ZEvesTactics.CommandSequence
getMessage() - Method in class net.sourceforge.czt.zeves.response.ZEvesErrorMessage
getMessages() - Method in class net.sourceforge.czt.zeves.response.ZEvesError
getName() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesLetDef
getName() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesOp
getName() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesReplace
getName() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesAbbrevDef
getName() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesBranch
getName() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesHorSchDef
getNameClass() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesName
getNameSource(String) - Method in class net.sourceforge.czt.zeves.ZEvesApi: Queries Z/EVES for the source paragraph (submitted by the user) introducing the given name.
getParents(List<Parent>) - Static method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter: Returns a comma-separated list of toolkit names, where standard Z toolkit names are not included as they are loaded in Z/EVES by default.
getPort() - Method in class net.sourceforge.czt.zeves.ZEvesApi
getPort() - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
getPosition() - Method in interface net.sourceforge.czt.zeves.snapshot.ISnapshotEntry
getPreviousEntry() - Method in interface net.sourceforge.czt.zeves.snapshot.ISnapshotEntry
getPreviousProofEntry(ISnapshotEntry, boolean) - Static method in class net.sourceforge.czt.zeves.snapshot.SnapshotUtil
getProof() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesTheorem
getProofCase() - Method in class net.sourceforge.czt.zeves.response.ZEvesOutput: Retrieves the proof case, if this information is available.
getProofScripts(String) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter: For every zproof available, return corresponding proof scripts
getProofStepIndex() - Method in class net.sourceforge.czt.zeves.snapshot.SnapshotData
getProofTrace() - Method in class net.sourceforge.czt.zeves.response.ZEvesOutput
getResult() - Method in class net.sourceforge.czt.zeves.snapshot.SnapshotData
getResults() - Method in class net.sourceforge.czt.zeves.response.ZEvesOutput
getRulesMatchingExpression(String, int, String) - Method in class net.sourceforge.czt.zeves.ZEvesApi
getRulesMatchingPredicate(String, int, String) - Method in class net.sourceforge.czt.zeves.ZEvesApi
getSectionInfo() - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Retrieves the section info associated with current (last added) snapshot entries.
getSectionInfo() - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
getSectionName() - Method in interface net.sourceforge.czt.zeves.snapshot.ISnapshotEntry
getSectionName() - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot.FileSection
getSections() - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Retrieves the list of sections that have entries in the snapshot
getServer() - Method in class net.sourceforge.czt.zeves.ZEvesServerEvent
getServerAddress() - Method in class net.sourceforge.czt.zeves.ZEvesApi
getTacticCommands(ProofCommand, ProofCommandVisitor<String>) - Static method in class net.sourceforge.czt.zeves.proof.ZEvesTactics
getTerm() - Method in class net.sourceforge.czt.zeves.snapshot.SnapshotData
getTheorem(String) - Method in class net.sourceforge.czt.zeves.ZEvesApi: Queries Z/EVES for theorem contents.
getTheoremNames(int) - Method in class net.sourceforge.czt.zeves.ZEvesApi
getTheoremOrigin(String) - Method in class net.sourceforge.czt.zeves.ZEvesApi
getThmNamesWithProofScripts() - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
getTrace() - Method in class net.sourceforge.czt.zeves.snapshot.SnapshotData
getTraceContents() - Method in class net.sourceforge.czt.zeves.response.ZEvesProofTrace: Retrieves trace contents - the parsed trace.
getTraceElements(ZEvesProofTrace.TraceType) - Method in class net.sourceforge.czt.zeves.response.ZEvesProofTrace: Retrieves Z/EVES trace elements for a particular trace type, e.g.
getType() - Method in class net.sourceforge.czt.zeves.response.ZEvesError
getType() - Method in interface net.sourceforge.czt.zeves.snapshot.ISnapshotEntry
getType() - Method in class net.sourceforge.czt.zeves.snapshot.SnapshotChangedEvent
getType(String, ZName) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
getValue() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesNumber
getValue() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesResponseString
getZEvesError() - Method in exception net.sourceforge.czt.zeves.ZEvesException
getZPrinter() - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
getZSect() - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
goal() - Method in class net.sourceforge.czt.zeves.snapshot.SnapshotData.Builder
GOAL_STEP_INDEX - Static variable in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot
goalName(String) - Method in class net.sourceforge.czt.zeves.snapshot.SnapshotData.Builder

H

hasContext() - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
hashCode() - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot.FileSection
HIDE_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} expression => getExpr(term.getExpr()); {1} name list => getZNameList.accept(this);

I

IgnorableCommand(String, boolean, boolean) - Constructor for class net.sourceforge.czt.zeves.proof.ZEvesTactics.IgnorableCommand
INFIX_APPL_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {1} expression => getExpr(ZUtils.getApplExprArguments(term).get(0)); {0} rel => getExpr(ZUtils.getApplExprRef(term)); {2} expression => getExpr(ZUtils.getApplExprArguments(term).get(1));
INFIX_REF_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} expression => getExpr(term.getZExprList().get(0)); {1} rel => getName(term.getZName()); {2} expression => getExpr(term.getZExprList().get(1));
isConnected() - Method in class net.sourceforge.czt.zeves.ZEvesApi
isConnected() - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
isEmpty() - Method in class net.sourceforge.czt.zeves.response.ZEvesOutput
isEmpty() - Method in class net.sourceforge.czt.zeves.response.ZEvesProofTrace
ISnapshotChangedListener - Interface in net.sourceforge.czt.zeves.snapshot
ISnapshotEntry - Interface in net.sourceforge.czt.zeves.snapshot
isRunning() - Method in class net.sourceforge.czt.zeves.ZEvesServer
isSchemaTyped(String, ZName) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
isSectionCompleted(String, String) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Checks if the given section is marked completed (i.e.
isStopOnError() - Method in class net.sourceforge.czt.zeves.proof.ZEvesTactics.IgnorableCommand
isStopOnNoEffect() - Method in class net.sourceforge.czt.zeves.proof.ZEvesTactics.IgnorableCommand
isUser() - Method in class net.sourceforge.czt.zeves.ZEvesServerEvent

L

LABEL_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = ability => label.getAbility(); {1} = usage => label.getUsage(); {2} = theorem-name => label.getTheoremName();
LAMBDA_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
LATEX_MARKUP_DIRECTIVE_COMMENT - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
LET_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} let-def => getLetDef(term.getSchText()); {1} expression => getExpr(term.getExpr());
loadContext() - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.

Called upon (re)connection.
LOCATION_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = Line => locAnn.getLine(); {1} = Column => locAnn.getCol(); {2} = Start-offset => locAnn.getStart(); {3} = End-offset => locAnn.getEnd(); {4} = lenGth => locAnn.getLength(); {5} = sourCe => locAnn.getLoc();

M

main(String[]) - Static method in class net.sourceforge.czt.zeves.CZT2ZEves
MEMPRED_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} expression => getExpr(term.getLeftExpr()); {1} rel => getRel(term); = "∈" | getRelOp(term) | "=" {2} expression => getExpr(term.getRightExpr()); Note: getRel implements the MemPred cases in the order they appear in Z.xsd
MemPredKind - Enum in net.sourceforge.czt.zeves.z
MIXFIX_APPL_EXPR_RELIMAGE_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} expression => getExpr(ZUtils.getApplExprArguments(term).get(0)); {1} expression => getExpr(ZUtils.getApplExprArguments(term).get(1));

N

needUndo(String, int) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Checks whether undo is necessary if updates are to be done at the given offset of file.
NEG_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} expression => getExpr(term.getExpr());
NEG_PRED_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = predicate => getPred(term.getPred());
net.sourceforge.czt.zeves - package net.sourceforge.czt.zeves
net.sourceforge.czt.zeves.proof - package net.sourceforge.czt.zeves.proof
net.sourceforge.czt.zeves.response - package net.sourceforge.czt.zeves.response
net.sourceforge.czt.zeves.response.form - package net.sourceforge.czt.zeves.response.form
net.sourceforge.czt.zeves.response.para - package net.sourceforge.czt.zeves.response.para
net.sourceforge.czt.zeves.snapshot - package net.sourceforge.czt.zeves.snapshot
net.sourceforge.czt.zeves.z - package net.sourceforge.czt.zeves.z
NL_SEP - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
NUM_STROKE_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = number => term.getNumber().toString()

O

OEPRATOR_TEMPLATE_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
OPERATOR_TEMPLATE_COMMENT - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns

P

POSTFIX_APPL_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} expression => getExpr(term.getLeftExpr()); {1} expression => getExpr(term.getRightExpr()); NOTE: No parenthesis for the postfix operator.
POSTFIX_REF_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
POWER_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} expression => getExpr(term.getExpr()); NOTE: For Z/EVES XML, CZT PowerExpr is just a special kind of var-name within expression-3, as there is no specific production for it.
PRE_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} expression => getExpr(term.getExpr()); NOTE: For Z/EVES this is a schema-ref, which here is simply a RefExpr.
PREDICATE_PARA_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = labelled-predicate => getAxiomPart(term.getPred); with label option enabled.
PREFIX_REF_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} rel => getName(term.getZName()); {1} expression => getExpr(term.getZExprList().get(0));
print(ZEvesResponsePrinter) - Method in class net.sourceforge.czt.zeves.response.ZEvesProverCmd
print(Object) - Method in interface net.sourceforge.czt.zeves.response.ZEvesResponsePrinter: Print the Z/EVES response XML element to a String
print(Term, SectionInfo, boolean) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
print(Term) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter: Top-level method which translates the given CZT term to a corresponding Z/EVES server XML API.
printSpec(Spec, SectionInfo, boolean) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
printSpec(Spec) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
printZSect(ZSect, SectionInfo, boolean) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
printZSect(ZSect) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
processCommand(String) - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
proofStep(int) - Method in class net.sourceforge.czt.zeves.snapshot.SnapshotData.Builder

Q

QNT_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
QNT_PRED_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = quantifier => getQntName(term); = "&exists;" | "&exists1;" | "∀" {1} = schema-text => term.getSchText.accept(this); {2} = predicate => getPred(term.getPred());

R

readXml(String) - Method in class net.sourceforge.czt.zeves.response.ZEvesResponseReader
reconnect() - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
RefExprKind - Enum in net.sourceforge.czt.zeves.z
removeServerListener(ZEvesServerListener) - Method in class net.sourceforge.czt.zeves.ZEvesServer
removeSnapshotChangedListener(ISnapshotChangedListener) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot
RENAME_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = expr => getExpr(term.getExpr()); {1} = rename list => getExpr(term.getExpr());
reset() - Method in class net.sourceforge.czt.zeves.ZEvesApi
result(Object) - Method in class net.sourceforge.czt.zeves.snapshot.SnapshotData.Builder
retry() - Method in class net.sourceforge.czt.zeves.ZEvesApi
ROMAN_NAMES - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
ROMAN_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
runPrinter(String, boolean, boolean) - Static method in class net.sourceforge.czt.zeves.CZT2ZEves
runZEves(String, String, int) - Static method in class net.sourceforge.czt.zeves.CZT2ZEves

S

SC_SEP - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: VARIOUS STRINGS USED AS Z/EVES XML PATTERNS FOR FORMATTING OPERATIONS
SCHEMA_BOX_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = schema-name => getSchName(((ConstDecl)term.getZSchText().getZDeclList()).getZName()); {3} = generic formals => NL_SEP + getGenFormals(term.getZName()); {4} = decl-part => getDeclPart(((SchExpr)((ConstDecl)term.getZSchText().getZDeclList()).getExpr()).getZSchText().getZDeclList()); {5} = axiom-part => getAxiomPart(((SchExpr)((ConstDecl)term.getZSchText().getZDeclList()).getExpr()).getSchText().getPred());
send(String) - Method in class net.sourceforge.czt.zeves.ZEvesApi: Sends a command to the server, formatted as specified in Z/EVES XML API requirements.
sendAbort() - Method in class net.sourceforge.czt.zeves.ZEvesApi: Sends an abort command to stop executing current command.
sendCommand(String, String...) - Method in class net.sourceforge.czt.zeves.ZEvesApi: Sends the indicated command to the server, passing arguments as command contents.
sendProofCommand(String) - Method in class net.sourceforge.czt.zeves.ZEvesApi
serverStarted(ZEvesServerEvent) - Method in interface net.sourceforge.czt.zeves.ZEvesServerListener
serverStopped(ZEvesServerEvent) - Method in interface net.sourceforge.czt.zeves.ZEvesServerListener
setContext(SectionInfo) - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
setContext(String, SectionInfo) - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
setCurrentGoalName(String) - Method in class net.sourceforge.czt.zeves.ZEvesApi
setHost(String) - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
setPort(int) - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
setPrintNarrParaAsComment(boolean) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
setSectionInfo(SectionInfo) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
setSectionName(String) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
snapshotChanged(SnapshotChangedEvent) - Method in interface net.sourceforge.czt.zeves.snapshot.ISnapshotChangedListener
SnapshotChangedEvent - Class in net.sourceforge.czt.zeves.snapshot
SnapshotChangedEvent(Object, SnapshotChangedEvent.SnapshotChangeType, List<? extends ISnapshotEntry>) - Constructor for class net.sourceforge.czt.zeves.snapshot.SnapshotChangedEvent
SnapshotChangedEvent.SnapshotChangeType - Enum in net.sourceforge.czt.zeves.snapshot
SnapshotData - Class in net.sourceforge.czt.zeves.snapshot
SnapshotData.Builder - Class in net.sourceforge.czt.zeves.snapshot
SnapshotUtil - Class in net.sourceforge.czt.zeves.snapshot
SnapshotUtil() - Constructor for class net.sourceforge.czt.zeves.snapshot.SnapshotUtil
specToZEvesXML(Spec, SectionInfo, boolean) - Static method in class net.sourceforge.czt.zeves.CZT2ZEves: Prints all the contenmts of the given specification and its sections a list of Z/EVES strings to be sent through the Z/EVES server one by one.
start() - Method in class net.sourceforge.czt.zeves.ZEvesServer
stop() - Method in class net.sourceforge.czt.zeves.ZEvesServer

T

termToZEvesXML(Term, SectionInfo, boolean) - Static method in class net.sourceforge.czt.zeves.CZT2ZEves: Prints the given term in Z/EVES XML format, provided it is a paragraph, predicate, declaration, or expression.
THEOREM_DEF_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = usage => getUsage(term); {3} = theorem-name => getTheoremName(term); {4} = generic formals => NL_SEP + getGenFormals(term.getZName()); {5} = axiom-part => getAxiomPart(term.getPred()); {6} = proof-part => getProofPart(term); Note: Provided axiom-part is not empty.
THETA_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} expression => getExpr(term.getExpr()); {1} strokes => getStrokes(term.getZStrokeList()); NOTE: The expression can represent either a schema-ref dealt with through RefExpr or DecorExpr, or schema-ref replacements dealt with through a RenameExpr.
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesApplication
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesBinder
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesBlurb
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesDecl
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesDisplay
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesIf
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesLet
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesLetDef
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesName
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesNumber
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesOp
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesParenForm
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesRelChain
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesRename
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesReplace
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesResponseString
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesSchemaText
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesSchemaType
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesSchName
toString() - Method in class net.sourceforge.czt.zeves.response.form.ZEvesTheoremRef
toString() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesAbbrevDef
toString() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesAxDef
toString() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesBranch
toString() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesFreeTypeDef
toString() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesGivenDef
toString() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesHorSchDef
toString() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesLabeledForm
toString() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesSchemaDef
toString() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesSynDef
toString() - Method in class net.sourceforge.czt.zeves.response.para.ZEvesTheorem
toString() - Method in class net.sourceforge.czt.zeves.response.ZEvesError
toString() - Method in class net.sourceforge.czt.zeves.response.ZEvesErrorMessage
toString() - Method in class net.sourceforge.czt.zeves.response.ZEvesOutput
toString() - Method in class net.sourceforge.czt.zeves.response.ZEvesProverCmd
toString() - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
trace(List<? extends ZEvesOutput>) - Method in class net.sourceforge.czt.zeves.snapshot.SnapshotData.Builder
translate(Term) - Method in class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
tryConnecting(int) - Method in class net.sourceforge.czt.zeves.ZEvesApi
TUPLESEL_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} expression => getExpr(term.getExpr()); {1} number => term.getSelect().toString(); NOTE: To avoid problems, we always enclosed the expression within parenthesis.

U

UNARY_MINUS_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
UNARY_MINUS_PLUS_INFIX_APPL_EXPR_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
undoBackThrough(int) - Method in class net.sourceforge.czt.zeves.ZEvesApi
undoBackTo(int) - Method in class net.sourceforge.czt.zeves.ZEvesApi
undoThrough(ZEvesApi, String, int) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Undoes Z/EVES commands up to (and including) the given offset.
undoThrough(ZEvesApi, ZEvesSnapshot.FileSection) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Undoes Z/EVES commands up to (and including) the given section.
UNLIMITED - Static variable in class net.sourceforge.czt.zeves.proof.ZEvesTactics.CommandSequence: A predefined constant to indicate unlimited loop of commands
UNPRINTABLE_PREDICATE - Static variable in class net.sourceforge.czt.zeves.response.ZEvesOutput
updatingSection(Position, String, String, SectionManager) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Mark the given section (filePath + sectionName) to be updating.
updatingSectionError(Position, String, String, SectionManager, SnapshotData) - Method in class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot: Mark the given section (filePath + sectionName) to be updating.
USAGE_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = Usage => label.getUsage();

V

valueOf(String) - Static method in enum net.sourceforge.czt.zeves.response.form.ZEvesBinder.BinderType: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.response.form.ZEvesDisplay.DisplayType: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.response.form.ZEvesKind: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.response.form.ZEvesName.NameClass: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.response.form.ZEvesName.NameScope: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.response.form.ZEvesName.NameStyle: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.response.form.ZEvesOp.OpType: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.response.para.ZEvesAbbrevDef.AbbrevType: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.response.para.ZEvesAbility: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.response.para.ZEvesUsage: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.response.ZEvesError.ZEvesErrorType: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.response.ZEvesProofTrace.TraceType: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.snapshot.SnapshotChangedEvent.SnapshotChangeType: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot.ResultType: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.z.MemPredKind: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.z.RefExprKind: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum net.sourceforge.czt.zeves.ZEvesApi.ZEvesTheoremType: Returns the enum constant of this type with the specified name.
values() - Static method in enum net.sourceforge.czt.zeves.response.form.ZEvesBinder.BinderType: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.response.form.ZEvesDisplay.DisplayType: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.response.form.ZEvesKind: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.response.form.ZEvesName.NameClass: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.response.form.ZEvesName.NameScope: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.response.form.ZEvesName.NameStyle: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.response.form.ZEvesOp.OpType: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.response.para.ZEvesAbbrevDef.AbbrevType: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.response.para.ZEvesAbility: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.response.para.ZEvesUsage: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.response.ZEvesError.ZEvesErrorType: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.response.ZEvesProofTrace.TraceType: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.snapshot.SnapshotChangedEvent.SnapshotChangeType: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot.ResultType: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.z.MemPredKind: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.z.RefExprKind: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum net.sourceforge.czt.zeves.ZEvesApi.ZEvesTheoremType: Returns an array containing the constants of this enum type, in the order they are declared.
visitApplExpr(ApplExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter: A function application (C.6.21, C.6.22).
visitApplyCommand(ApplyCommand) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitAxPara(AxPara) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitBindExpr(BindExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitBindSelExpr(BindSelExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitCaseAnalysisCommand(CaseAnalysisCommand) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitCondExpr(CondExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitConjPara(ConjPara) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitDecorExpr(DecorExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitExprPred(ExprPred) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitFalsePred(FalsePred) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitFreePara(FreePara) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitFreetype(Freetype) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitGivenPara(GivenPara) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitHideExpr(HideExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitInclDecl(InclDecl) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitInstantiation(Instantiation) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitInstantiationList(InstantiationList) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitInStroke(InStroke) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitLambdaExpr(LambdaExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitLatexMarkupPara(LatexMarkupPara) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitLetExpr(LetExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitMemPred(MemPred) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitMuExpr(MuExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitNarrPara(NarrPara) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitNegExpr(NegExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitNegPred(NegPred) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitNewOldPair(NewOldPair) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitNextStroke(NextStroke) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitNormalizationCommand(NormalizationCommand) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitNumExpr(NumExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitNumStroke(NumStroke) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitOptempPara(OptempPara) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitOutStroke(OutStroke) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitPowerExpr(PowerExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitPred2(Pred2) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitPreExpr(PreExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitProdExpr(ProdExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitProofCommand(ProofCommand) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitProofScript(ProofScript) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitQntExpr(QntExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitQntPred(QntPred) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitQuantifiersCommand(QuantifiersCommand) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitRefExpr(RefExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitRenameExpr(RenameExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitSchExpr(SchExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitSchExpr2(SchExpr2) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitSetCompExpr(SetCompExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitSetExpr(SetExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitSimplificationCommand(SimplificationCommand) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitSorryCommand(SorryCommand) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitSubstitutionCommand(SubstitutionCommand) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitTerm(Term) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitThetaExpr(ThetaExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitTruePred(TruePred) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitTupleExpr(TupleExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitTupleSelExpr(TupleSelExpr) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitUnparsedPara(UnparsedPara) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitUseCommand(UseCommand) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitVarDecl(VarDecl) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitWithCommand(WithCommand) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitZDeclList(ZDeclList) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter: Represents the declaration production.
visitZExprList(ZExprList) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter: Represents the expression-list production.
visitZName(ZName) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitZRenameList(ZRenameList) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter
visitZSchText(ZSchText) - Method in class net.sourceforge.czt.zeves.z.CZT2ZEvesPrinter

W

withParentheses(Object) - Static method in class net.sourceforge.czt.zeves.response.ZEvesResponseUtil

X

XmlAnyElementItem - Class in net.sourceforge.czt.zeves.response: Similar to XmlAnyElementList, but for a single item, because we cannot have a wrapper on a single item.
XmlAnyElementItem() - Constructor for class net.sourceforge.czt.zeves.response.XmlAnyElementItem
XmlAnyElementList - Class in net.sourceforge.czt.zeves.response: A special list to act for XmlAnyElement wrappers, because currently one cannot have the following annotations: @XmlElementWrapper @XmlAnyElement - they fail to unmarshall.
XmlAnyElementList() - Constructor for class net.sourceforge.czt.zeves.response.XmlAnyElementList

Z

Z_TOOLKIT_NAMES - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
ZED_BOX_FREETYPE_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = zboxItemFreeType=> Build from getBranch for each branch.
ZED_BOX_GIVENSET_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = zboxItemNameList=> getIdentList(term.getZNames());
ZED_BOX_HORIZONTAL_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = zboxItemName => getSchName(((ConstDecl)term.getZSchText().getZDeclList()).getZName()); | getDefLHS(((ConstDecl)term.getZSchText().getZDeclList()).getZName()); {3} = gen-formals => getGenFormals(term.getZName()); {4} = zboxItemSymbol => "&eqhat;" | "==" {5} = zboxItemExpr => getExpr(((ConstDecl)term.getZSchText().getZDeclList()).getExpr()); For postix, genformals appear early.
ZED_BOX_INFIXGENOP_HORIZONTAL_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
ZEves - Class in net.sourceforge.czt.zeves
ZEves() - Constructor for class net.sourceforge.czt.zeves.ZEves
ZEVES_COMMAND - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: Main XML API command for Z/EVES.
ZEVES_PROOF_PART_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns
ZEVES_TOOLKIT_NAME - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: Z/EVES toolkit overrides CZT toolkits.
ZEvesAbbrevDef - Class in net.sourceforge.czt.zeves.response.para: abbreviation definition (var-name, prefix generic, infix generic)
ZEvesAbbrevDef() - Constructor for class net.sourceforge.czt.zeves.response.para.ZEvesAbbrevDef
ZEvesAbbrevDef.AbbrevType - Enum in net.sourceforge.czt.zeves.response.para
ZEvesAbility - Enum in net.sourceforge.czt.zeves.response.para
ZEvesApi - Class in net.sourceforge.czt.zeves: This class is provides calls to Z/EVES XML-based API, where communication is done via sockets.
ZEvesApi(String, int) - Constructor for class net.sourceforge.czt.zeves.ZEvesApi
ZEvesApi.ZEvesTheoremType - Enum in net.sourceforge.czt.zeves
ZEvesApplication - Class in net.sourceforge.czt.zeves.response.form
ZEvesApplication() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesApplication
ZEvesAxDef - Class in net.sourceforge.czt.zeves.response.para: axiomatic and generic definition
ZEvesAxDef() - Constructor for class net.sourceforge.czt.zeves.response.para.ZEvesAxDef
ZEvesBinder - Class in net.sourceforge.czt.zeves.response.form: In a number of places, the kind of the expression is indicated with an attribute rather than with a tag (e.g., binders).
ZEvesBinder() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesBinder
ZEvesBinder.BinderType - Enum in net.sourceforge.czt.zeves.response.form
ZEvesBlurb - Class in net.sourceforge.czt.zeves.response.form
ZEvesBlurb() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesBlurb
ZEvesBranch - Class in net.sourceforge.czt.zeves.response.para
ZEvesBranch() - Constructor for class net.sourceforge.czt.zeves.response.para.ZEvesBranch
ZEvesDecl - Class in net.sourceforge.czt.zeves.response.form
ZEvesDecl() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesDecl
ZEvesDisplay - Class in net.sourceforge.czt.zeves.response.form
ZEvesDisplay() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesDisplay
ZEvesDisplay.DisplayType - Enum in net.sourceforge.czt.zeves.response.form
ZEvesError - Class in net.sourceforge.czt.zeves.response
ZEvesError() - Constructor for class net.sourceforge.czt.zeves.response.ZEvesError
ZEvesError.ZEvesErrorType - Enum in net.sourceforge.czt.zeves.response
ZEvesErrorMessage - Class in net.sourceforge.czt.zeves.response
ZEvesErrorMessage() - Constructor for class net.sourceforge.czt.zeves.response.ZEvesErrorMessage
ZEvesException - Exception in net.sourceforge.czt.zeves
ZEvesException() - Constructor for exception net.sourceforge.czt.zeves.ZEvesException
ZEvesException(String) - Constructor for exception net.sourceforge.czt.zeves.ZEvesException
ZEvesException(Throwable) - Constructor for exception net.sourceforge.czt.zeves.ZEvesException
ZEvesException(String, Throwable) - Constructor for exception net.sourceforge.czt.zeves.ZEvesException
ZEvesException(String, Throwable, String) - Constructor for exception net.sourceforge.czt.zeves.ZEvesException
ZEvesException(ZEvesError) - Constructor for exception net.sourceforge.czt.zeves.ZEvesException
ZEvesException(ZEvesError, String) - Constructor for exception net.sourceforge.czt.zeves.ZEvesException
ZEvesFreeTypeDef - Class in net.sourceforge.czt.zeves.response.para: free type definition
ZEvesFreeTypeDef() - Constructor for class net.sourceforge.czt.zeves.response.para.ZEvesFreeTypeDef
ZEvesGivenDef - Class in net.sourceforge.czt.zeves.response.para: Given set declaration
ZEvesGivenDef() - Constructor for class net.sourceforge.czt.zeves.response.para.ZEvesGivenDef
ZEvesHorSchDef - Class in net.sourceforge.czt.zeves.response.para: schema definition (horizontal)
ZEvesHorSchDef() - Constructor for class net.sourceforge.czt.zeves.response.para.ZEvesHorSchDef
ZEvesIf - Class in net.sourceforge.czt.zeves.response.form
ZEvesIf() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesIf
ZEvesIncompatibleASTException - Exception in net.sourceforge.czt.zeves: Exception thrown whenever the tool finds a Z Standard term that cannot be converted to Z/EVES Z.
ZEvesIncompatibleASTException(String) - Constructor for exception net.sourceforge.czt.zeves.ZEvesIncompatibleASTException: Creates a new instance of ZEvesIncompatibleASTException
ZEvesIncompatibleASTException(String, Throwable) - Constructor for exception net.sourceforge.czt.zeves.ZEvesIncompatibleASTException
ZEvesIncompatibleASTException(Throwable) - Constructor for exception net.sourceforge.czt.zeves.ZEvesIncompatibleASTException
ZEvesIncompatibleASTException(String, Term) - Constructor for exception net.sourceforge.czt.zeves.ZEvesIncompatibleASTException
ZEvesKind - Enum in net.sourceforge.czt.zeves.response.form
ZEvesLabeledForm - Class in net.sourceforge.czt.zeves.response.para
ZEvesLabeledForm() - Constructor for class net.sourceforge.czt.zeves.response.para.ZEvesLabeledForm
ZEvesLet - Class in net.sourceforge.czt.zeves.response.form
ZEvesLet() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesLet
ZEvesLetDef - Class in net.sourceforge.czt.zeves.response.form
ZEvesLetDef() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesLetDef
ZEvesName - Class in net.sourceforge.czt.zeves.response.form: The name element represents a variable or constant name.
ZEvesName() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesName
ZEvesName.NameClass - Enum in net.sourceforge.czt.zeves.response.form
ZEvesName.NameScope - Enum in net.sourceforge.czt.zeves.response.form
ZEvesName.NameStyle - Enum in net.sourceforge.czt.zeves.response.form
ZEvesNumber - Class in net.sourceforge.czt.zeves.response.form
ZEvesNumber() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesNumber
ZEvesOp - Class in net.sourceforge.czt.zeves.response.form
ZEvesOp() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesOp
ZEvesOp.OpType - Enum in net.sourceforge.czt.zeves.response.form
ZEvesOutput - Class in net.sourceforge.czt.zeves.response
ZEvesOutput() - Constructor for class net.sourceforge.czt.zeves.response.ZEvesOutput
ZEvesParenForm - Class in net.sourceforge.czt.zeves.response.form: Schema expressions, predicates, and expressions are not differentiated in this syntax; the only reason to do so would be to decide whether certain forms should be parenthesized (e.g., if expression vs.
ZEvesParenForm() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesParenForm
ZEvesProofTrace - Class in net.sourceforge.czt.zeves.response: A utility class that parses Z/EVES response trace (given as ZEvesBlurb object), and partitions the results according to trace type.
ZEvesProofTrace(ZEvesBlurb) - Constructor for class net.sourceforge.czt.zeves.response.ZEvesProofTrace
ZEvesProofTrace.TraceType - Enum in net.sourceforge.czt.zeves.response
ZEvesProverCmd - Class in net.sourceforge.czt.zeves.response: The provercmd form allows for the different kinds of commands to be represented.
ZEvesProverCmd() - Constructor for class net.sourceforge.czt.zeves.response.ZEvesProverCmd
ZEvesRelChain - Class in net.sourceforge.czt.zeves.response.form
ZEvesRelChain() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesRelChain
ZEvesRename - Class in net.sourceforge.czt.zeves.response.form
ZEvesRename() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesRename
ZEvesReplace - Class in net.sourceforge.czt.zeves.response.form
ZEvesReplace() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesReplace
ZEvesResponsePrinter - Interface in net.sourceforge.czt.zeves.response: An interface to provide printing facilities to Z/EVES Response XML elements.
ZEvesResponseReader - Class in net.sourceforge.czt.zeves.response: The reader parses Z/EVES response XML and produces appropriate Z/EVES Java objects with the data.
ZEvesResponseString - Class in net.sourceforge.czt.zeves.response.form
ZEvesResponseString() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesResponseString
ZEvesResponseUtil - Class in net.sourceforge.czt.zeves.response
ZEvesSchemaDef - Class in net.sourceforge.czt.zeves.response.para: schema definition (vertical)
ZEvesSchemaDef() - Constructor for class net.sourceforge.czt.zeves.response.para.ZEvesSchemaDef
ZEvesSchemaText - Class in net.sourceforge.czt.zeves.response.form
ZEvesSchemaText() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesSchemaText
ZEvesSchemaType - Class in net.sourceforge.czt.zeves.response.form
ZEvesSchemaType() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesSchemaType
ZEvesSchName - Class in net.sourceforge.czt.zeves.response.form: The schname element represents a schema name.
ZEvesSchName() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesSchName
ZEvesServer - Class in net.sourceforge.czt.zeves: The class for Z/EVES server process management.
ZEvesServer(String, int) - Constructor for class net.sourceforge.czt.zeves.ZEvesServer
ZEvesServer(String, int, File) - Constructor for class net.sourceforge.czt.zeves.ZEvesServer
ZEvesServerConnectionException - Exception in net.sourceforge.czt.zeves: Deprecated.
part of obsoleted ZEvesSocket implementation
ZEvesServerConnectionException(String) - Constructor for exception net.sourceforge.czt.zeves.ZEvesServerConnectionException: Deprecated.

Creates a new instance of ZEvesIncompatibleException
ZEvesServerConnectionException(String, Throwable) - Constructor for exception net.sourceforge.czt.zeves.ZEvesServerConnectionException: Deprecated.
ZEvesServerConnectionException(Throwable) - Constructor for exception net.sourceforge.czt.zeves.ZEvesServerConnectionException: Deprecated.
ZEvesServerEvent - Class in net.sourceforge.czt.zeves
ZEvesServerEvent(ZEvesServer, boolean) - Constructor for class net.sourceforge.czt.zeves.ZEvesServerEvent
ZEvesServerListener - Interface in net.sourceforge.czt.zeves
ZEvesSnapshot - Class in net.sourceforge.czt.zeves.snapshot: This class represent a snapshot of Z/EVES submit state.
ZEvesSnapshot() - Constructor for class net.sourceforge.czt.zeves.snapshot.ZEvesSnapshot
ZEvesSnapshot.FileSection - Class in net.sourceforge.czt.zeves.snapshot: Immutable structure to identify section within its file.
ZEvesSnapshot.ResultType - Enum in net.sourceforge.czt.zeves.snapshot
ZEvesSocket - Class in net.sourceforge.czt.zeves: Deprecated.
use ZEvesApi
ZEvesSocket() - Constructor for class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.
ZEvesSocket(boolean) - Constructor for class net.sourceforge.czt.zeves.ZEvesSocket: Deprecated.

Creates a new instance of ZEvesEvaluator
ZEvesSynDef - Class in net.sourceforge.czt.zeves.response.para
ZEvesSynDef() - Constructor for class net.sourceforge.czt.zeves.response.para.ZEvesSynDef
ZEvesTactics - Class in net.sourceforge.czt.zeves.proof: A support for Z/EVES tactic commands, which can be defined as a sequence (or loop) of existing Z/EVES commands.
ZEvesTactics() - Constructor for class net.sourceforge.czt.zeves.proof.ZEvesTactics
ZEvesTactics.CommandSequence - Class in net.sourceforge.czt.zeves.proof: A wrapper for a sequence of Z/EVES proof commands.
ZEvesTactics.IgnorableCommand - Class in net.sourceforge.czt.zeves.proof: A pair of Z/EVES command string (converted to XML representation) and whether it should stop if not effective.
ZEvesTheorem - Class in net.sourceforge.czt.zeves.response.para: theorem
ZEvesTheorem() - Constructor for class net.sourceforge.czt.zeves.response.para.ZEvesTheorem
ZEvesTheoremRef - Class in net.sourceforge.czt.zeves.response.form: theoremref represents a theorem reference, and is used only in a prover command (use).
ZEvesTheoremRef() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesTheoremRef
ZEvesType - Class in net.sourceforge.czt.zeves.response.form: Many forms allow for an optional "type" child element; this can be included if output is to be fully annotated with type information.
ZEvesType() - Constructor for class net.sourceforge.czt.zeves.response.form.ZEvesType
ZEvesUsage - Enum in net.sourceforge.czt.zeves.response.para
ZEvesXmlEntities - Class in net.sourceforge.czt.zeves.response
ZEvesXmlEntities() - Constructor for class net.sourceforge.czt.zeves.response.ZEvesXmlEntities
ZEvesXMLPatterns - Interface in net.sourceforge.czt.zeves.z
ZSECTION_BEGIN_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns: {0} string => term.getName(); {1} parents list => getParents(term.getParent()); {2} paragraphs => getParas(term.getPara());
ZSECTION_END_PATTERN - Static variable in interface net.sourceforge.czt.zeves.z.ZEvesXMLPatterns

A B C D E F G H I L M N O P Q R S T U V W X Z