Package net.sourceforge.czt.zeves.ast

Interfaces of the AST for ZEves.

See: Description

Interface Summary

Interface	Description
ApplyCommand	Theorem application commands.
CaseAnalysisCommand	Goal splitting and case analysis commands.
ComplexCommand	Abstract complex command.
Instantiation	Encapsulates one instantiation or replacement for the instantiate or use commands.
InstantiationCommand	Abstract command for instantiations.
InstantiationList	List of possible instantiations.
NormalizationCommand	Term rewriting via normal forms.
ProofCommand	Abstract proof command
ProofCommandInfo
ProofCommandInfoList
ProofCommandList
ProofScript	Sequence of proof commands
ProofType	Proof command information collected to form a proof script type.
QuantifiersCommand	Quantifier manipulation and elimination.
SimplificationCommand	Term rewriting and simplification commands of various kinds.
SorryCommand	Sorry and Oops - virtual - commands; inspired by Isabelle's meanings: sorry is give up on proving, yet keep the theorem; oops, gives up on proving, but don't keep the theorem albeit leave the goal.
SubstitutionCommand	Term substitution commands.
UseCommand	Theorem / axiom introduction with particular parameters / instantiations.
WithCommand	Compound commands involving either specific theorem names and/or expressions/predicates.
WrappedCommand	Abstract proof command that wraps up another proof command within it.
ZEvesFactory	The object factory for the AST.
ZEvesLabel	Label to theorems and axiomatic predicates
ZEvesNote	Notes and comments from the user within formal text (not type checked)

Enum Summary

Enum	Description
CaseAnalysisKind	A(n) CaseAnalysisKind enumeration.
InstantiationKind	A(n) InstantiationKind enumeration.
LabelAbility	A(n) LabelAbility enumeration.
LabelUsage	A(n) LabelUsage enumeration.
NormalizationKind	A(n) NormalizationKind enumeration.
ProofStepKind	A(n) ProofStepKind enumeration.
ProofStepScope	A(n) ProofStepScope enumeration.
RewriteKind	A(n) RewriteKind enumeration.
RewritePower	A(n) RewritePower enumeration.
SubstitutionKind	A(n) SubstitutionKind enumeration.

Package net.sourceforge.czt.zeves.ast Description

Interfaces of the AST for ZEves. See net.sourceforge.czt.base.ast for an overview over the AST for Z.