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 * Initial Definition of operator. This is a basic predicate constant. For example: 23 * "x is element of y". 24 * 25 * @author Michael Meyling 26 */ 27 public interface InitialPredicateDefinition extends NodeType { 28 29 /** 30 * Get number of arguments for the defined object. Carries information about the argument 31 * number the defined object needs. 32 * 33 * @return Argument number. 34 */ 35 public String getArgumentNumber(); 36 37 /** 38 * This name together with {@link #getArgumentNumber()} identifies a predicate. 39 * 40 * @return Name of defined predicate. 41 */ 42 public String getName(); 43 44 /** 45 * Get LaTeX output for definition. The replaceable arguments must are marked as "#1", 46 * "#2" and so on. For example "\mathfrak{M}(#1)" 47 * 48 * @return LaTeX pattern for definition type setting. 49 */ 50 public String getLatexPattern(); 51 52 /** 53 * Get new predicate constant with free subject variables. The predicate constant must 54 * match {@link #getName()} and {@link #getArgumentNumber()}. 55 * 56 * @return Predicate constant with free subject variables. 57 */ 58 public Element getPredCon(); 59 60 /** 61 * Get description. Optional. 62 * 63 * @return Description. Might be <code>null</code>. 64 */ 65 public LatexList getDescription(); 66 67 }