1
/* Copyright (C) 2006, 2007 William McCune
3
This file is part of the LADR Deduction Library.
5
The LADR Deduction Library is free software; you can redistribute it
6
and/or modify it under the terms of the GNU General Public License,
9
The LADR Deduction Library is distributed in the hope that it will be
10
useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
11
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12
GNU General Public License for more details.
14
You should have received a copy of the GNU General Public License
15
along with the LADR Deduction Library; if not, write to the Free Software
16
Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
28
/* Public definitions */
30
/* End of public definitions */
32
/* Public function prototypes from basic.c */
34
void init_basic_paramod(void);
36
void set_basic_paramod(BOOL flag);
38
BOOL basic_paramod(void);
40
void mark_term_nonbasic(Term t);
42
void mark_all_nonbasic(Term t);
44
BOOL nonbasic_term(Term t);
46
BOOL basic_term(Term t);
48
int nonbasic_flag(void);
50
Term apply_basic(Term t, Context c);
52
Term apply_basic_substitute(Term t, Term beta, Context c_from,
53
Term into_term, Context c_into);
55
void clear_all_nonbasic_marks(Term t);
57
void p_term_basic(Term t);
59
#endif /* conditional compilation of whole file */