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

All Superinterfaces:

NodeType

All Known Implementing Classes:

InitialFunctionDefinitionVo

public interface InitialFunctionDefinition
extends NodeType

Definition of initial function operator. This is a function constant that can not defined further. For example the function "emptySet" might be an undefinable function of a certain set theory. So every model for this set theory must mark an object of its domain as "emptySet".

Author:

Michael Meyling

Method Summary

java.lang.String	getArgumentNumber() Get number of arguments for the defined object.
LatexList	getDescription() Get description.
Element	getFunCon() Get function constant that we define.
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.

getFunCon

Element getFunCon()

Get function constant that we define. The function constant must match getName() and getArgumentNumber().

Returns:

Function constant with free subject variables as arguments.

getDescription

LatexList getDescription()

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

Returns:

Description.