Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
0   67   0   -
0   8   -   0
0     -  
1    
 
  FunctionDefinition       Line # 25 0 0 - -1.0
 
No Tests
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2013, 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    }