1 /* This file is part of the project "Hilbert II" - http://www.qedeq.org" target="alexandria_uri">http://www.qedeq.org
2 *
3 * Copyright 2000-2014, Michael Meyling <mime@qedeq.org>.
4 *
5 * "Hilbert II" is free software; you can redistribute
6 * it and/or modify it under the terms of the GNU General Public
7 * License as published by the Free Software Foundation; either
8 * version 2 of the License, or (at your option) any later version.
9 *
10 * This program is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 */
15
16 package org.qedeq.kernel.se.base.module;
17
18 import org.qedeq.kernel.se.base.list.Element;
19
20
21 /**
22 * Definition of initial function operator. This is a function constant that can not defined further.
23 * For example the function "emptySet" might be an undefinable function of a certain set theory. So every
24 * model for this set theory must mark an object of its domain as "emptySet".
25 *
26 * @author Michael Meyling
27 */
28 public interface InitialFunctionDefinition extends NodeType {
29
30 /**
31 * Get number of arguments for the defined object. Carries information about the argument
32 * number the defined object needs.
33 *
34 * @return Argument number.
35 */
36 public String getArgumentNumber();
37
38 /**
39 * This name together with {@link #getArgumentNumber()} identifies a function.
40 *
41 * @return Name of defined function.
42 */
43 public String getName();
44
45 /**
46 * Get LaTeX output for definition. The replaceable arguments must are marked as "#1",
47 * "#2" and so on. For example "\mathfrak{M}(#1)"
48 *
49 * @return LaTeX pattern for definition type setting.
50 */
51 public String getLatexPattern();
52
53 /**
54 * Get function constant that we define. The function constant must
55 * match {@link #getName()} and {@link #getArgumentNumber()}.
56 *
57 * @return Function constant with free subject variables as arguments.
58 */
59 public Element getFunCon();
60
61 /**
62 * Get description. Only necessary if formula is not self-explanatory.
63 *
64 * @return Description.
65 */
66 public LatexList getDescription();
67
68 }