org.qedeq.kernel.se.base.module
Interface FunctionDefinition

All Superinterfaces:

NodeType

All Known Implementing Classes:

FunctionDefinitionVo

public interface FunctionDefinition
extends NodeType

Definition of function operator. This is a function constant. For example the function "x union y" or constants like the empty set.

Author:

Michael Meyling

Method Summary

java.lang.String	getArgumentNumber() Get number of arguments for the defined object.
LatexList	getDescription() Get description.
Formula	getFormula() Get defining formula for function constant.
java.lang.String	getLatexPattern() Get LaTeX output for definition.
java.lang.String	getName() This name together with getArgumentNumber() identifies a function.

Methods inherited from interface org.qedeq.kernel.se.base.module.NodeType

getAxiom, getFunctionDefinition, getInitialFunctionDefinition, getInitialPredicateDefinition, getPredicateDefinition, getProposition, getRule

Method Detail

getArgumentNumber

java.lang.String getArgumentNumber()

Get number of arguments for the defined object. Carries information about the argument number the defined object needs.

Returns:

Argument number.

getName

java.lang.String getName()

This name together with getArgumentNumber() identifies a function.

Returns:

Name of defined function.

getLatexPattern

java.lang.String getLatexPattern()

Get LaTeX output for definition. The replaceable arguments must are marked as "#1", "#2" and so on. For example "\mathfrak{M}(#1)"

Returns:

LaTeX pattern for definition type setting.

getFormula

Formula getFormula()

Get defining formula for function constant. This might be for example: f(x, y) = {z | z \in x & z \in y} Such a formula must have the equal operator as first operator. The first operand must be the function with free (and pairwise different) subject variables as arguments.

Returns:

Defining formula for function constant.

getDescription

LatexList getDescription()

Get description. Only necessary if formula is not self-explanatory.

Returns:

Description.