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
19 /**
20 * Definition of operator. This is a predicate constant. For example the
21 * predicate "x is a set" could be defined in MK with the formula "\exists y: x \in y".
22 * <p>
23 * There must also be the possibility to define basic predicate constants like
24 * "x is element of y".
25 *
26 * @author Michael Meyling
27 */
28 public interface PredicateDefinition 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 predicate.
40 *
41 * @return Name of defined predicate.
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 complete formula. That is an equivalence between the new predicate and
55 * the defining formula.
56 *
57 * @return Complete formula.
58 */
59 public Formula getFormula();
60
61 /**
62 * Get description. Only necessary if formula is not self-explanatory.
63 *
64 * @return Description.
65 */
66 public LatexList getDescription();
67
68 }