| Class | Description |
|---|---|
| ZEvesApplication | |
| ZEvesBinder |
In a number of places, the kind of the expression is indicated with an
attribute rather than with a tag (e.g., binders).
|
| ZEvesBlurb | |
| ZEvesDecl | |
| ZEvesDisplay | |
| ZEvesIf | |
| ZEvesLet | |
| ZEvesLetDef | |
| ZEvesName |
The name element represents a variable or constant name.
|
| ZEvesNumber | |
| ZEvesOp | |
| ZEvesParenForm |
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.
|
| ZEvesRelChain | |
| ZEvesRename | |
| ZEvesReplace | |
| ZEvesResponseString | |
| ZEvesSchemaText | |
| ZEvesSchemaType | |
| ZEvesSchName |
The schname element represents a schema name.
|
| ZEvesTheoremRef |
theoremref represents a theorem reference, and is used only in a prover command (use).
|
| ZEvesType |
Many forms allow for an optional "type" child element; this can be included
if output is to be fully annotated with type information.
|
| Enum | Description |
|---|---|
| ZEvesBinder.BinderType | |
| ZEvesDisplay.DisplayType | |
| ZEvesKind | |
| ZEvesName.NameClass | |
| ZEvesName.NameScope | |
| ZEvesName.NameStyle | |
| ZEvesOp.OpType |
Copyright © 2003–2016 Community Z Tools Project. All rights reserved.