Interface ImetamathListener

This interface defines a complete listener for a parse tree produced by metamathParser.

Namespace: GCore.Antlr.Grammers.Metamath
Assembly: Metamath.dll
Syntax
public interface ImetamathListener : Antlr4.Runtime.Tree.IParseTreeListener

Methods

| Improve this Doc View Source

EnterAssertstmt(metamathParser.AssertstmtContext)

Enter a parse tree produced by assertstmt().

Declaration
void EnterAssertstmt(metamathParser.AssertstmtContext context)
Parameters
Type Name Description
metamathParser.AssertstmtContext context

The parse tree.
| Improve this Doc View Source

EnterAxiomstmt(metamathParser.AxiomstmtContext)

Enter a parse tree produced by axiomstmt().

Declaration
void EnterAxiomstmt(metamathParser.AxiomstmtContext context)
Parameters
Type Name Description
metamathParser.AxiomstmtContext context

The parse tree.
| Improve this Doc View Source

EnterBlock(metamathParser.BlockContext)

Enter a parse tree produced by block().

Declaration
void EnterBlock(metamathParser.BlockContext context)
Parameters
Type Name Description
metamathParser.BlockContext context

The parse tree.
| Improve this Doc View Source

EnterCompressedproof(metamathParser.CompressedproofContext)

Enter a parse tree produced by compressedproof().

Declaration
void EnterCompressedproof(metamathParser.CompressedproofContext context)
Parameters
Type Name Description
metamathParser.CompressedproofContext context

The parse tree.
| Improve this Doc View Source

EnterConstant(metamathParser.ConstantContext)

Enter a parse tree produced by constant().

Declaration
void EnterConstant(metamathParser.ConstantContext context)
Parameters
Type Name Description
metamathParser.ConstantContext context

The parse tree.
| Improve this Doc View Source

EnterConstantstmt(metamathParser.ConstantstmtContext)

Enter a parse tree produced by constantstmt().

Declaration
void EnterConstantstmt(metamathParser.ConstantstmtContext context)
Parameters
Type Name Description
metamathParser.ConstantstmtContext context

The parse tree.
| Improve this Doc View Source

EnterDatabase(metamathParser.DatabaseContext)

Enter a parse tree produced by database().

Declaration
void EnterDatabase(metamathParser.DatabaseContext context)
Parameters
Type Name Description
metamathParser.DatabaseContext context

The parse tree.
| Improve this Doc View Source

EnterDisjointstmt(metamathParser.DisjointstmtContext)

Enter a parse tree produced by disjointstmt().

Declaration
void EnterDisjointstmt(metamathParser.DisjointstmtContext context)
Parameters
Type Name Description
metamathParser.DisjointstmtContext context

The parse tree.
| Improve this Doc View Source

EnterEssentialstmt(metamathParser.EssentialstmtContext)

Enter a parse tree produced by essentialstmt().

Declaration
void EnterEssentialstmt(metamathParser.EssentialstmtContext context)
Parameters
Type Name Description
metamathParser.EssentialstmtContext context

The parse tree.
| Improve this Doc View Source

EnterFilename(metamathParser.FilenameContext)

Enter a parse tree produced by filename().

Declaration
void EnterFilename(metamathParser.FilenameContext context)
Parameters
Type Name Description
metamathParser.FilenameContext context

The parse tree.
| Improve this Doc View Source

EnterFloatingstmt(metamathParser.FloatingstmtContext)

Enter a parse tree produced by floatingstmt().

Declaration
void EnterFloatingstmt(metamathParser.FloatingstmtContext context)
Parameters
Type Name Description
metamathParser.FloatingstmtContext context

The parse tree.
| Improve this Doc View Source

EnterHypothesisstmt(metamathParser.HypothesisstmtContext)

Enter a parse tree produced by hypothesisstmt().

Declaration
void EnterHypothesisstmt(metamathParser.HypothesisstmtContext context)
Parameters
Type Name Description
metamathParser.HypothesisstmtContext context

The parse tree.
| Improve this Doc View Source

EnterIncludestmt(metamathParser.IncludestmtContext)

Enter a parse tree produced by includestmt().

Declaration
void EnterIncludestmt(metamathParser.IncludestmtContext context)
Parameters
Type Name Description
metamathParser.IncludestmtContext context

The parse tree.
| Improve this Doc View Source

EnterMathsymbol(metamathParser.MathsymbolContext)

Enter a parse tree produced by mathsymbol().

Declaration
void EnterMathsymbol(metamathParser.MathsymbolContext context)
Parameters
Type Name Description
metamathParser.MathsymbolContext context

The parse tree.
| Improve this Doc View Source

EnterOutermostscopestmt(metamathParser.OutermostscopestmtContext)

Enter a parse tree produced by outermostscopestmt().

Declaration
void EnterOutermostscopestmt(metamathParser.OutermostscopestmtContext context)
Parameters
Type Name Description
metamathParser.OutermostscopestmtContext context

The parse tree.
| Improve this Doc View Source

EnterProof(metamathParser.ProofContext)

Enter a parse tree produced by proof().

Declaration
void EnterProof(metamathParser.ProofContext context)
Parameters
Type Name Description
metamathParser.ProofContext context

The parse tree.
| Improve this Doc View Source

EnterProvablestmt(metamathParser.ProvablestmtContext)

Enter a parse tree produced by provablestmt().

Declaration
void EnterProvablestmt(metamathParser.ProvablestmtContext context)
Parameters
Type Name Description
metamathParser.ProvablestmtContext context

The parse tree.
| Improve this Doc View Source

EnterStmt(metamathParser.StmtContext)

Enter a parse tree produced by stmt().

Declaration
void EnterStmt(metamathParser.StmtContext context)
Parameters
Type Name Description
metamathParser.StmtContext context

The parse tree.
| Improve this Doc View Source

EnterTypecode(metamathParser.TypecodeContext)

Enter a parse tree produced by typecode().

Declaration
void EnterTypecode(metamathParser.TypecodeContext context)
Parameters
Type Name Description
metamathParser.TypecodeContext context

The parse tree.
| Improve this Doc View Source

EnterUncompressedproof(metamathParser.UncompressedproofContext)

Enter a parse tree produced by uncompressedproof().

Declaration
void EnterUncompressedproof(metamathParser.UncompressedproofContext context)
Parameters
Type Name Description
metamathParser.UncompressedproofContext context

The parse tree.
| Improve this Doc View Source

EnterVariable(metamathParser.VariableContext)

Enter a parse tree produced by variable().

Declaration
void EnterVariable(metamathParser.VariableContext context)
Parameters
Type Name Description
metamathParser.VariableContext context

The parse tree.
| Improve this Doc View Source

EnterVariablestmt(metamathParser.VariablestmtContext)

Enter a parse tree produced by variablestmt().

Declaration
void EnterVariablestmt(metamathParser.VariablestmtContext context)
Parameters
Type Name Description
metamathParser.VariablestmtContext context

The parse tree.
| Improve this Doc View Source

ExitAssertstmt(metamathParser.AssertstmtContext)

Exit a parse tree produced by assertstmt().

Declaration
void ExitAssertstmt(metamathParser.AssertstmtContext context)
Parameters
Type Name Description
metamathParser.AssertstmtContext context

The parse tree.
| Improve this Doc View Source

ExitAxiomstmt(metamathParser.AxiomstmtContext)

Exit a parse tree produced by axiomstmt().

Declaration
void ExitAxiomstmt(metamathParser.AxiomstmtContext context)
Parameters
Type Name Description
metamathParser.AxiomstmtContext context

The parse tree.
| Improve this Doc View Source

ExitBlock(metamathParser.BlockContext)

Exit a parse tree produced by block().

Declaration
void ExitBlock(metamathParser.BlockContext context)
Parameters
Type Name Description
metamathParser.BlockContext context

The parse tree.
| Improve this Doc View Source

ExitCompressedproof(metamathParser.CompressedproofContext)

Exit a parse tree produced by compressedproof().

Declaration
void ExitCompressedproof(metamathParser.CompressedproofContext context)
Parameters
Type Name Description
metamathParser.CompressedproofContext context

The parse tree.
| Improve this Doc View Source

ExitConstant(metamathParser.ConstantContext)

Exit a parse tree produced by constant().

Declaration
void ExitConstant(metamathParser.ConstantContext context)
Parameters
Type Name Description
metamathParser.ConstantContext context

The parse tree.
| Improve this Doc View Source

ExitConstantstmt(metamathParser.ConstantstmtContext)

Exit a parse tree produced by constantstmt().

Declaration
void ExitConstantstmt(metamathParser.ConstantstmtContext context)
Parameters
Type Name Description
metamathParser.ConstantstmtContext context

The parse tree.
| Improve this Doc View Source

ExitDatabase(metamathParser.DatabaseContext)

Exit a parse tree produced by database().

Declaration
void ExitDatabase(metamathParser.DatabaseContext context)
Parameters
Type Name Description
metamathParser.DatabaseContext context

The parse tree.
| Improve this Doc View Source

ExitDisjointstmt(metamathParser.DisjointstmtContext)

Exit a parse tree produced by disjointstmt().

Declaration
void ExitDisjointstmt(metamathParser.DisjointstmtContext context)
Parameters
Type Name Description
metamathParser.DisjointstmtContext context

The parse tree.
| Improve this Doc View Source

ExitEssentialstmt(metamathParser.EssentialstmtContext)

Exit a parse tree produced by essentialstmt().

Declaration
void ExitEssentialstmt(metamathParser.EssentialstmtContext context)
Parameters
Type Name Description
metamathParser.EssentialstmtContext context

The parse tree.
| Improve this Doc View Source

ExitFilename(metamathParser.FilenameContext)

Exit a parse tree produced by filename().

Declaration
void ExitFilename(metamathParser.FilenameContext context)
Parameters
Type Name Description
metamathParser.FilenameContext context

The parse tree.
| Improve this Doc View Source

ExitFloatingstmt(metamathParser.FloatingstmtContext)

Exit a parse tree produced by floatingstmt().

Declaration
void ExitFloatingstmt(metamathParser.FloatingstmtContext context)
Parameters
Type Name Description
metamathParser.FloatingstmtContext context

The parse tree.
| Improve this Doc View Source

ExitHypothesisstmt(metamathParser.HypothesisstmtContext)

Exit a parse tree produced by hypothesisstmt().

Declaration
void ExitHypothesisstmt(metamathParser.HypothesisstmtContext context)
Parameters
Type Name Description
metamathParser.HypothesisstmtContext context

The parse tree.
| Improve this Doc View Source

ExitIncludestmt(metamathParser.IncludestmtContext)

Exit a parse tree produced by includestmt().

Declaration
void ExitIncludestmt(metamathParser.IncludestmtContext context)
Parameters
Type Name Description
metamathParser.IncludestmtContext context

The parse tree.
| Improve this Doc View Source

ExitMathsymbol(metamathParser.MathsymbolContext)

Exit a parse tree produced by mathsymbol().

Declaration
void ExitMathsymbol(metamathParser.MathsymbolContext context)
Parameters
Type Name Description
metamathParser.MathsymbolContext context

The parse tree.
| Improve this Doc View Source

ExitOutermostscopestmt(metamathParser.OutermostscopestmtContext)

Exit a parse tree produced by outermostscopestmt().

Declaration
void ExitOutermostscopestmt(metamathParser.OutermostscopestmtContext context)
Parameters
Type Name Description
metamathParser.OutermostscopestmtContext context

The parse tree.
| Improve this Doc View Source

ExitProof(metamathParser.ProofContext)

Exit a parse tree produced by proof().

Declaration
void ExitProof(metamathParser.ProofContext context)
Parameters
Type Name Description
metamathParser.ProofContext context

The parse tree.
| Improve this Doc View Source

ExitProvablestmt(metamathParser.ProvablestmtContext)

Exit a parse tree produced by provablestmt().

Declaration
void ExitProvablestmt(metamathParser.ProvablestmtContext context)
Parameters
Type Name Description
metamathParser.ProvablestmtContext context

The parse tree.
| Improve this Doc View Source

ExitStmt(metamathParser.StmtContext)

Exit a parse tree produced by stmt().

Declaration
void ExitStmt(metamathParser.StmtContext context)
Parameters
Type Name Description
metamathParser.StmtContext context

The parse tree.
| Improve this Doc View Source

ExitTypecode(metamathParser.TypecodeContext)

Exit a parse tree produced by typecode().

Declaration
void ExitTypecode(metamathParser.TypecodeContext context)
Parameters
Type Name Description
metamathParser.TypecodeContext context

The parse tree.
| Improve this Doc View Source

ExitUncompressedproof(metamathParser.UncompressedproofContext)

Exit a parse tree produced by uncompressedproof().

Declaration
void ExitUncompressedproof(metamathParser.UncompressedproofContext context)
Parameters
Type Name Description
metamathParser.UncompressedproofContext context

The parse tree.
| Improve this Doc View Source

ExitVariable(metamathParser.VariableContext)

Exit a parse tree produced by variable().

Declaration
void ExitVariable(metamathParser.VariableContext context)
Parameters
Type Name Description
metamathParser.VariableContext context

The parse tree.
| Improve this Doc View Source

ExitVariablestmt(metamathParser.VariablestmtContext)

Exit a parse tree produced by variablestmt().

Declaration
void ExitVariablestmt(metamathParser.VariablestmtContext context)
Parameters
Type Name Description
metamathParser.VariablestmtContext context

The parse tree.