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 function operator. This is a function constant. For example the function 21 * "x union y" or constants like the empty set. 22 * 23 * @author Michael Meyling 24 */ 25 public interface FunctionDefinition extends NodeType { 26 27 /** 28 * Get number of arguments for the defined object. Carries information about the argument 29 * number the defined object needs. 30 * 31 * @return Argument number. 32 */ 33 public String getArgumentNumber(); 34 35 /** 36 * This name together with {@link #getArgumentNumber()} identifies a function. 37 * 38 * @return Name of defined function. 39 */ 40 public String getName(); 41 42 /** 43 * Get LaTeX output for definition. The replaceable arguments must are marked as "#1", 44 * "#2" and so on. For example "\mathfrak{M}(#1)" 45 * 46 * @return LaTeX pattern for definition type setting. 47 */ 48 public String getLatexPattern(); 49 50 /** 51 * Get defining formula for function constant. This might be for example: 52 * f(x, y) = {z | z \in x & z \in y} 53 * Such a formula must have the equal operator as first operator. The first operand must be 54 * the function with free (and pairwise different) subject variables as arguments. 55 * 56 * @return Defining formula for function constant. 57 */ 58 public Formula getFormula(); 59 60 /** 61 * Get description. Only necessary if formula is not self-explanatory. 62 * 63 * @return Description. 64 */ 65 public LatexList getDescription(); 66 67 }