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

All Known Implementing Classes:

BasicZEvesTranslator, CZT2ZEvesPrinter
```
public interface ZEvesXMLPatterns
```
Author:

leo

Field Summary

Fields
Modifier and Type	Field and Description
`static String`	`ABILITY_PATTERN` {0} = Ability => label.getAbility();
`static String`	`APPL_EXPR_BAG_PATTERN`
`static String`	`APPL_EXPR_PATTERN` {0} expression => getExpr(term.getLeftExpr()); {1} expression => getExpr(term.getRightExpr()); NOTE: Added parentheses on the argument, because it may bind stronger than the expression.
`static String`	`APPL_EXPR_SEQ_PATTERN` {0} comma sep list of expressions from getExpr(ZUtils.getApplExprArguments(term).get(n));
`static String`	`AXIOMATIC_BOX_PATTERN` {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = decl-part => getDeclPart(term.getZSchText().getZDeclList()); {3} = axiom-part => getAxiomPart(term.getSchText().getPred());
`static String`	`BIN_PRED_PATTERN` {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.
`static String`	`BIN_SCHEXPR_PATTERN` {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.
`static String`	`BIND_EXPR_PATTERN` {0} semi-colon sep list of bindings as NAME : EXPR ; NAME : EXPR ...
`static String`	`BINDSEL_EXPR_PATTERN`
`static String`	`BRANCH_PATTERN` {0} = var-name => getVarName(term.getZName()); {1} = expr => getExpr(term.getExpr());
`static String`	`COMMENT_PATTERN`
`static String`	`COND_EXPR_PATTERN` {0} predicate => getPred(term.getPred()); {1} expression => getExpr(term.getLeftExpr()); {2} expression => getExpr(term.getRightExpr());
`static String`	`EQ_SIGN`
`static String`	`EQ_SUBST_APPL_EXPR_PATTERN`
`static String`	`GENERIC_BOX_PATTERN` {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());
`static String`	`HIDE_EXPR_PATTERN` {0} expression => getExpr(term.getExpr()); {1} name list => getZNameList.accept(this);
`static String`	`INFIX_APPL_EXPR_PATTERN` {1} expression => getExpr(ZUtils.getApplExprArguments(term).get(0)); {0} rel => getExpr(ZUtils.getApplExprRef(term)); {2} expression => getExpr(ZUtils.getApplExprArguments(term).get(1));
`static String`	`INFIX_REF_EXPR_PATTERN` {0} expression => getExpr(term.getZExprList().get(0)); {1} rel => getName(term.getZName()); {2} expression => getExpr(term.getZExprList().get(1));
`static String`	`LABEL_PATTERN` {0} = ability => label.getAbility(); {1} = usage => label.getUsage(); {2} = theorem-name => label.getTheoremName();
`static String`	`LAMBDA_EXPR_PATTERN`
`static String`	`LATEX_MARKUP_DIRECTIVE_COMMENT`
`static String`	`LET_EXPR_PATTERN` {0} let-def => getLetDef(term.getSchText()); {1} expression => getExpr(term.getExpr());
`static String`	`LOCATION_PATTERN` {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();
`static String`	`MEMPRED_PATTERN` {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
`static String`	`MIXFIX_APPL_EXPR_RELIMAGE_PATTERN` {0} expression => getExpr(ZUtils.getApplExprArguments(term).get(0)); {1} expression => getExpr(ZUtils.getApplExprArguments(term).get(1));
`static String`	`NEG_EXPR_PATTERN` {0} expression => getExpr(term.getExpr());
`static String`	`NEG_PRED_PATTERN` {0} = predicate => getPred(term.getPred());
`static String`	`NL_SEP`
`static String`	`NUM_STROKE_PATTERN` {0} = number => term.getNumber().toString()
`static String`	`OEPRATOR_TEMPLATE_PATTERN`
`static String`	`OPERATOR_TEMPLATE_COMMENT`
`static String`	`POSTFIX_APPL_EXPR_PATTERN` {0} expression => getExpr(term.getLeftExpr()); {1} expression => getExpr(term.getRightExpr()); NOTE: No parenthesis for the postfix operator.
`static String`	`POSTFIX_REF_EXPR_PATTERN`
`static String`	`POWER_EXPR_PATTERN` {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.
`static String`	`PRE_EXPR_PATTERN` {0} expression => getExpr(term.getExpr()); NOTE: For Z/EVES this is a schema-ref, which here is simply a RefExpr.
`static String`	`PREDICATE_PARA_PATTERN` {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = labelled-predicate => getAxiomPart(term.getPred); with label option enabled.
`static String`	`PREFIX_REF_EXPR_PATTERN` {0} rel => getName(term.getZName()); {1} expression => getExpr(term.getZExprList().get(0));
`static String`	`QNT_EXPR_PATTERN`
`static String`	`QNT_PRED_PATTERN` {0} = quantifier => getQntName(term); = "&exists;" \| "&exists1;" \| "∀" {1} = schema-text => term.getSchText.accept(this); {2} = predicate => getPred(term.getPred());
`static String`	`RENAME_EXPR_PATTERN` {0} = expr => getExpr(term.getExpr()); {1} = rename list => getExpr(term.getExpr());
`static List<String>`	`ROMAN_NAMES`
`static String`	`ROMAN_PATTERN`
`static String`	`SC_SEP` VARIOUS STRINGS USED AS Z/EVES XML PATTERNS FOR FORMATTING OPERATIONS
`static String`	`SCHEMA_BOX_PATTERN` {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());
`static String`	`THEOREM_DEF_PATTERN` {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.
`static String`	`THETA_EXPR_PATTERN` {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.
`static String`	`TUPLESEL_EXPR_PATTERN` {0} expression => getExpr(term.getExpr()); {1} number => term.getSelect().toString(); NOTE: To avoid problems, we always enclosed the expression within parenthesis.
`static String`	`UNARY_MINUS_EXPR_PATTERN`
`static String`	`UNARY_MINUS_PLUS_INFIX_APPL_EXPR_PATTERN`
`static String`	`USAGE_PATTERN` {0} = Usage => label.getUsage();
`static List<String>`	`Z_TOOLKIT_NAMES`
`static String`	`ZED_BOX_FREETYPE_PATTERN` {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = zboxItemFreeType=> Build from getBranch for each branch.
`static String`	`ZED_BOX_GIVENSET_PATTERN` {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = zboxItemNameList=> getIdentList(term.getZNames());
`static String`	`ZED_BOX_HORIZONTAL_PATTERN` {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.
`static String`	`ZED_BOX_INFIXGENOP_HORIZONTAL_PATTERN`
`static String`	`ZEVES_COMMAND` Main XML API command for Z/EVES.
`static String`	`ZEVES_PROOF_PART_PATTERN`
`static String`	`ZEVES_TOOLKIT_NAME` Z/EVES toolkit overrides CZT toolkits.
`static String`	`ZSECTION_BEGIN_PATTERN` {0} string => term.getName(); {1} parents list => getParents(term.getParent()); {2} paragraphs => getParas(term.getPara());
`static String`	`ZSECTION_END_PATTERN`

- Field Detail
  - SC_SEP
```
static final String SC_SEP
```
    VARIOUS STRINGS USED AS Z/EVES XML PATTERNS FOR FORMATTING OPERATIONS
    
    See Also:
    
    Constant Field Values
  - EQ_SIGN
```
static final String EQ_SIGN
```
    See Also:
    
    Constant Field Values
  - NL_SEP
```
static final String NL_SEP
```
  - ZEVES_COMMAND
```
static final String ZEVES_COMMAND
```
    Main XML API command for Z/EVES. DO NOT INCLUDE NL before/after {1}.
    
    See Also:
    
    Constant Field Values
  - COMMENT_PATTERN
```
static final String COMMENT_PATTERN
```
    See Also:
    
    Constant Field Values
  - OPERATOR_TEMPLATE_COMMENT
```
static final String OPERATOR_TEMPLATE_COMMENT
```
    See Also:
    
    Constant Field Values
  - OEPRATOR_TEMPLATE_PATTERN
```
static final String OEPRATOR_TEMPLATE_PATTERN
```
    See Also:
    
    Constant Field Values
  - LATEX_MARKUP_DIRECTIVE_COMMENT
```
static final String LATEX_MARKUP_DIRECTIVE_COMMENT
```
    See Also:
    
    Constant Field Values
  - ZEVES_PROOF_PART_PATTERN
```
static final String ZEVES_PROOF_PART_PATTERN
```
    See Also:
    
    Constant Field Values
  - ZSECTION_BEGIN_PATTERN
```
static final String ZSECTION_BEGIN_PATTERN
```
    {0} string => term.getName(); {1} parents list => getParents(term.getParent()); {2} paragraphs => getParas(term.getPara());
    
    See Also:
    
    Constant Field Values
  - ZSECTION_END_PATTERN
```
static final String ZSECTION_END_PATTERN
```
    See Also:
    
    Constant Field Values
  - ZEVES_TOOLKIT_NAME
```
static final String ZEVES_TOOLKIT_NAME
```
    Z/EVES toolkit overrides CZT toolkits.
    
    See Also:
    
    Constant Field Values
  - Z_TOOLKIT_NAMES
```
static final List<String> Z_TOOLKIT_NAMES
```
  - NUM_STROKE_PATTERN
```
static final String NUM_STROKE_PATTERN
```
    {0} = number => term.getNumber().toString()
    
    See Also:
    
    Constant Field Values
  - BRANCH_PATTERN
```
static final String BRANCH_PATTERN
```
    {0} = var-name => getVarName(term.getZName()); {1} = expr => getExpr(term.getExpr());
    
    See Also:
    
    Constant Field Values
  - ZED_BOX_HORIZONTAL_PATTERN
```
static final String ZED_BOX_HORIZONTAL_PATTERN
```
    {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. For prefix, we have a different production with an extra parameter
    
    See Also:
    
    Constant Field Values
  - ZED_BOX_INFIXGENOP_HORIZONTAL_PATTERN
```
static final String ZED_BOX_INFIXGENOP_HORIZONTAL_PATTERN
```
    See Also:
    
    Constant Field Values
  - ZED_BOX_GIVENSET_PATTERN
```
static final String ZED_BOX_GIVENSET_PATTERN
```
    {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = zboxItemNameList=> getIdentList(term.getZNames());
    
    See Also:
    
    Constant Field Values
  - ZED_BOX_FREETYPE_PATTERN
```
static final String ZED_BOX_FREETYPE_PATTERN
```
    {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = zboxItemFreeType=> Build from getBranch for each branch.
    
    See Also:
    
    Constant Field Values
  - PREDICATE_PARA_PATTERN
```
static final String PREDICATE_PARA_PATTERN
```
    {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = labelled-predicate => getAxiomPart(term.getPred); with label option enabled.
    
    See Also:
    
    Constant Field Values
  - AXIOMATIC_BOX_PATTERN
```
static final String AXIOMATIC_BOX_PATTERN
```
    {0} = location => getLocation(term); {1} = ability => getAbility(term); {2} = decl-part => getDeclPart(term.getZSchText().getZDeclList()); {3} = axiom-part => getAxiomPart(term.getSchText().getPred());
    
    See Also:
    
    Constant Field Values
  - GENERIC_BOX_PATTERN
```
static final String GENERIC_BOX_PATTERN
```
    {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());
    
    See Also:
    
    Constant Field Values
  - SCHEMA_BOX_PATTERN
```
static final String SCHEMA_BOX_PATTERN
```
    {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());
    
    See Also:
    
    Constant Field Values
  - THEOREM_DEF_PATTERN
```
static final String THEOREM_DEF_PATTERN
```
    {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.
    
    See Also:
    
    Constant Field Values
  - LABEL_PATTERN
```
static final String LABEL_PATTERN
```
    {0} = ability => label.getAbility(); {1} = usage => label.getUsage(); {2} = theorem-name => label.getTheoremName();
    
    See Also:
    
    Constant Field Values
  - LOCATION_PATTERN
```
static final String LOCATION_PATTERN
```
    {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();
    
    See Also:
    
    Constant Field Values
  - ABILITY_PATTERN
```
static final String ABILITY_PATTERN
```
    {0} = Ability => label.getAbility();
    
    See Also:
    
    Constant Field Values
  - USAGE_PATTERN
```
static final String USAGE_PATTERN
```
    {0} = Usage => label.getUsage();
    
    See Also:
    
    Constant Field Values
  - NEG_PRED_PATTERN
```
static final String NEG_PRED_PATTERN
```
    {0} = predicate => getPred(term.getPred());
    
    See Also:
    
    Constant Field Values
  - QNT_PRED_PATTERN
```
static final String QNT_PRED_PATTERN
```
    {0} = quantifier => getQntName(term); = "&exists;" | "&exists1;" | "∀" {1} = schema-text => term.getSchText.accept(this); {2} = predicate => getPred(term.getPred());
    
    See Also:
    
    Constant Field Values
  - BIN_PRED_PATTERN
```
static final String BIN_PRED_PATTERN
```
    {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. each element on an AndPred having a Z/EVES label). For this case, we can only accept term.getOp() as And, Chain, or Semi, but not NL.
    
    See Also:
    
    Constant Field Values
  - MEMPRED_PATTERN
```
static final String MEMPRED_PATTERN
```
    {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
    
    See Also:
    
    Constant Field Values
  - NEG_EXPR_PATTERN
```
static final String NEG_EXPR_PATTERN
```
    {0} expression => getExpr(term.getExpr());
    
    See Also:
    
    Constant Field Values
  - LAMBDA_EXPR_PATTERN
```
static final String LAMBDA_EXPR_PATTERN
```
    See Also:
    
    Constant Field Values
  - QNT_EXPR_PATTERN
```
static final String QNT_EXPR_PATTERN
```
    See Also:
    
    Constant Field Values
  - LET_EXPR_PATTERN
```
static final String LET_EXPR_PATTERN
```
    {0} let-def => getLetDef(term.getSchText()); {1} expression => getExpr(term.getExpr());
    
    See Also:
    
    Constant Field Values
  - PRE_EXPR_PATTERN
```
static final String PRE_EXPR_PATTERN
```
    {0} expression => getExpr(term.getExpr()); NOTE: For Z/EVES this is a schema-ref, which here is simply a RefExpr. Nevertheless, care needs to be taken because in the translation of RefExpr as Z/EVES does not allow all forms of schema-expression that CZT allows.
    
    See Also:
    
    Constant Field Values
  - ROMAN_PATTERN
```
static final String ROMAN_PATTERN
```
    See Also:
    
    Constant Field Values
  - ROMAN_NAMES
```
static final List<String> ROMAN_NAMES
```
  - TUPLESEL_EXPR_PATTERN
```
static final String TUPLESEL_EXPR_PATTERN
```
    {0} expression => getExpr(term.getExpr()); {1} number => term.getSelect().toString(); NOTE: To avoid problems, we always enclosed the expression within parenthesis. If those are redundant, the prover will remove then appropriately. TODO: Check this or ask Mark Saaltink directly.
    
    See Also:
    
    Constant Field Values
  - BINDSEL_EXPR_PATTERN
```
static final String BINDSEL_EXPR_PATTERN
```
    See Also:
    
    Constant Field Values
  - COND_EXPR_PATTERN
```
static final String COND_EXPR_PATTERN
```
    {0} predicate => getPred(term.getPred()); {1} expression => getExpr(term.getLeftExpr()); {2} expression => getExpr(term.getRightExpr());
    
    See Also:
    
    Constant Field Values
  - THETA_EXPR_PATTERN
```
static final String THETA_EXPR_PATTERN
```
    {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.
    
    See Also:
    
    Constant Field Values
  - POWER_EXPR_PATTERN
```
static final String POWER_EXPR_PATTERN
```
    {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.
    
    See Also:
    
    Constant Field Values
  - BIN_SCHEXPR_PATTERN
```
static final String BIN_SCHEXPR_PATTERN
```
    {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.
    
    See Also:
    
    Constant Field Values
  - HIDE_EXPR_PATTERN
```
static final String HIDE_EXPR_PATTERN
```
    {0} expression => getExpr(term.getExpr()); {1} name list => getZNameList.accept(this);
    
    See Also:
    
    Constant Field Values
  - APPL_EXPR_PATTERN
```
static final String APPL_EXPR_PATTERN
```
    {0} expression => getExpr(term.getLeftExpr()); {1} expression => getExpr(term.getRightExpr()); NOTE: Added parentheses on the argument, because it may bind stronger than the expression. Also addded parentheses to the function, because it may be a complex expression
    
    See Also:
    
    Constant Field Values
  - EQ_SUBST_APPL_EXPR_PATTERN
```
static final String EQ_SUBST_APPL_EXPR_PATTERN
```
    See Also:
    
    Constant Field Values
  - UNARY_MINUS_EXPR_PATTERN
```
static final String UNARY_MINUS_EXPR_PATTERN
```
    See Also:
    
    Constant Field Values
  - POSTFIX_APPL_EXPR_PATTERN
```
static final String POSTFIX_APPL_EXPR_PATTERN
```
    {0} expression => getExpr(term.getLeftExpr()); {1} expression => getExpr(term.getRightExpr()); NOTE: No parenthesis for the postfix operator. For example, tilde symbol (inverse) needs to be without parentheses, otherwise Z/EVES throws an error.
    
    See Also:
    
    Constant Field Values
  - INFIX_APPL_EXPR_PATTERN
```
static final String INFIX_APPL_EXPR_PATTERN
```
    {1} expression => getExpr(ZUtils.getApplExprArguments(term).get(0)); {0} rel => getExpr(ZUtils.getApplExprRef(term)); {2} expression => getExpr(ZUtils.getApplExprArguments(term).get(1));
    
    See Also:
    
    Constant Field Values
  - UNARY_MINUS_PLUS_INFIX_APPL_EXPR_PATTERN
```
static final String UNARY_MINUS_PLUS_INFIX_APPL_EXPR_PATTERN
```
    See Also:
    
    Constant Field Values
  - APPL_EXPR_SEQ_PATTERN
```
static final String APPL_EXPR_SEQ_PATTERN
```
    {0} comma sep list of expressions from getExpr(ZUtils.getApplExprArguments(term).get(n));
    
    See Also:
    
    Constant Field Values
  - APPL_EXPR_BAG_PATTERN
```
static final String APPL_EXPR_BAG_PATTERN
```
    See Also:
    
    Constant Field Values
  - MIXFIX_APPL_EXPR_RELIMAGE_PATTERN
```
static final String MIXFIX_APPL_EXPR_RELIMAGE_PATTERN
```
    {0} expression => getExpr(ZUtils.getApplExprArguments(term).get(0)); {1} expression => getExpr(ZUtils.getApplExprArguments(term).get(1));
    
    See Also:
    
    Constant Field Values
  - INFIX_REF_EXPR_PATTERN
```
static final String INFIX_REF_EXPR_PATTERN
```
    {0} expression => getExpr(term.getZExprList().get(0)); {1} rel => getName(term.getZName()); {2} expression => getExpr(term.getZExprList().get(1));
    
    See Also:
    
    Constant Field Values
  - PREFIX_REF_EXPR_PATTERN
```
static final String PREFIX_REF_EXPR_PATTERN
```
    {0} rel => getName(term.getZName()); {1} expression => getExpr(term.getZExprList().get(0));
    
    See Also:
    
    Constant Field Values
  - POSTFIX_REF_EXPR_PATTERN
```
static final String POSTFIX_REF_EXPR_PATTERN
```
    See Also:
    
    Constant Field Values
  - BIND_EXPR_PATTERN
```
static final String BIND_EXPR_PATTERN
```
    {0} semi-colon sep list of bindings as NAME : EXPR ; NAME : EXPR ...
    
    See Also:
    
    Constant Field Values
  - RENAME_EXPR_PATTERN
```
static final String RENAME_EXPR_PATTERN
```
    {0} = expr => getExpr(term.getExpr()); {1} = rename list => getExpr(term.getExpr());
    
    See Also:
    
    Constant Field Values

Interface ZEvesXMLPatterns

Field Summary

Field Detail

SC_SEP

EQ_SIGN

NL_SEP

ZEVES_COMMAND

COMMENT_PATTERN

OPERATOR_TEMPLATE_COMMENT

OEPRATOR_TEMPLATE_PATTERN

LATEX_MARKUP_DIRECTIVE_COMMENT

ZEVES_PROOF_PART_PATTERN

ZSECTION_BEGIN_PATTERN

ZSECTION_END_PATTERN

ZEVES_TOOLKIT_NAME

Z_TOOLKIT_NAMES

NUM_STROKE_PATTERN

BRANCH_PATTERN

ZED_BOX_HORIZONTAL_PATTERN

ZED_BOX_INFIXGENOP_HORIZONTAL_PATTERN

ZED_BOX_GIVENSET_PATTERN

ZED_BOX_FREETYPE_PATTERN

PREDICATE_PARA_PATTERN

AXIOMATIC_BOX_PATTERN

GENERIC_BOX_PATTERN

SCHEMA_BOX_PATTERN

THEOREM_DEF_PATTERN

LABEL_PATTERN

LOCATION_PATTERN

ABILITY_PATTERN

USAGE_PATTERN

NEG_PRED_PATTERN

QNT_PRED_PATTERN

BIN_PRED_PATTERN

MEMPRED_PATTERN

NEG_EXPR_PATTERN

LAMBDA_EXPR_PATTERN

QNT_EXPR_PATTERN

LET_EXPR_PATTERN

PRE_EXPR_PATTERN

ROMAN_PATTERN

ROMAN_NAMES

TUPLESEL_EXPR_PATTERN

BINDSEL_EXPR_PATTERN

COND_EXPR_PATTERN

THETA_EXPR_PATTERN

POWER_EXPR_PATTERN

BIN_SCHEXPR_PATTERN

HIDE_EXPR_PATTERN

APPL_EXPR_PATTERN

EQ_SUBST_APPL_EXPR_PATTERN

UNARY_MINUS_EXPR_PATTERN

POSTFIX_APPL_EXPR_PATTERN

INFIX_APPL_EXPR_PATTERN

UNARY_MINUS_PLUS_INFIX_APPL_EXPR_PATTERN

APPL_EXPR_SEQ_PATTERN

APPL_EXPR_BAG_PATTERN

MIXFIX_APPL_EXPR_RELIMAGE_PATTERN

INFIX_REF_EXPR_PATTERN

PREFIX_REF_EXPR_PATTERN

POSTFIX_REF_EXPR_PATTERN

BIND_EXPR_PATTERN

RENAME_EXPR_PATTERN