[Imprint][Data Privacy Statement][E-Mail]

Back to the index. View project statistic. View project symbols. View KIV symbols to check that all symbols are available.

All project symbols

symbol	specification	entry
#	termfuns	function, term_or_none → nat
#	rawcontext	function, rawctxt → nat
#	term	function, term → nat
%	nat-div	function, nat × nat → nat
*	nat-mult	function, nat × nat → nat
+	nat-basic2	function, nat × nat → nat
+1	nat-basic1	function, nat → nat
-	nat	function, nat × nat → nat
-1	nat-basic1	function, nat → nat
.1	term	function, term → term
.2	term	function, term → term
.c	rawcontext	function, rawctxt → rawctxt
.t	term_or_none	function, term_or_none → term
.t	rawcontext	function, rawctxt → term
/	nat-div	function, nat × nat → nat
<	nat-basic1	predicate, nat × nat
=>	reduce	predicate, term × term
=>*	reduce	predicate, term × term
=>top	reduce	predicate, term × term
>	nat	predicate, nat × nat
C	rawcontext	variable, rawctxt
C0	rawcontext	variable, rawctxt
Ca	rawcontext	predicate, rawctxt
Cf	rawcontext	predicate, rawctxt
I	OUTREDUCE	constant, term
K	term	constant, term
O	rawcontext	constant, rawctxt
R	reduce	variable, term × term → bool
RED	OUTREDUCE	procedure, term : term
RED1	OUTREDUCE	procedure, term : term_or_none
S	term	constant, term
SII	OUTREDUCE	constant, term
TOPRED	OUTREDUCE	procedure, term : term_or_none
]	subst	function, rawctxt × term → term
^	reduce	function, term × term → bool × nat → term × term → bool
_	rawcontext	function, rawctxt × term → rawctxt
_	rawcontext	function, term × rawctxt → rawctxt
_	term	function, term × term → term
ap	term	predicate, term
context	context	predicate, rawctxt
even	nat-even	predicate, nat
hasS	termfuns	predicate, term_or_none
hasS	termfuns	predicate, term
irred	reduce	predicate, term
ks	termfuns	function, nat → term
m	nat-basic2	variable, nat
max	nat-even	function, nat × nat → nat
min	nat-even	function, nat × nat → nat
n	nat-basic1	variable, nat
n0	nat-basic1	variable, nat
n1	nat-basic1	variable, nat
nat	nat-basic1	sort,
none	term_or_none	constant, term_or_none
odd	nat-even	predicate, nat
rawctxt	rawcontext	sort,
some	term_or_none	function, term → term_or_none
t	term	variable, term
t'	reduce	variable, term
t0	term	variable, term
t1	term	variable, term
t2	term	variable, term
term	term	sort,
term_or_none	term_or_none	sort,
tn	term_or_none	variable, term_or_none
v	reduce	variable, term
v1	reduce	variable, term
v2	reduce	variable, term
v3	reduce	variable, term
value	value	predicate, term
≤	nat	predicate, nat × nat
≥	nat	predicate, nat × nat