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

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	references	f	referenceset → nat
# .	references	f	references → nat
#oc	references	f	reference × references → nat
. '	references	f	reference → references
. + .	nat-basic2	f	nat × nat → nat
. + .	references	f	reference × references → references
. + .	references	f	reference × reference → references
. + .	references	f	references × references → references
. + .	references	f	references × reference → references
. ++ .	references	f	referenceset × reference → referenceset
. ++ .	references	f	references × reference → references
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -- .	references	f	referenceset × reference → referenceset
. -1	nat-basic1	f	nat → nat
. -1l .	references	f	references × nat → references
. -1l .	references	f	references × reference → references
. -l .	references	f	references × reference → references
. .butlast	references	f	references → references
. .butmax	references	f	referenceset → referenceset
. .butmin	references	f	referenceset → referenceset
. .first	references	f	references → reference
. .last	references	f	references → reference
. .max	references	f	referenceset → reference
. .min	references	f	referenceset → reference
. .rest	references	f	references → references
. < .	references	p	referenceset × reference
. < .	references	p	reference × referenceset
. < .	references	p	references × references
. < .	reference	p	reference × reference
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	references	f	references × nat → reference
. [ . ]	references	f	references × nat × reference → references
. \ .	references	f	references × references → references
. \ .	references	f	referenceset × referenceset → referenceset
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ∈ .	references	p	reference × referenceset
. ∈ .	references	p	reference × references
. ∪ .	references	f	references × references → references
. ∪ .	references	f	referenceset × referenceset → referenceset
. ∩ .	references	f	referenceset × referenceset → referenceset
. ⊆ .	references	p	referenceset × referenceset
. ⊆ .	references	p	references × references
. ⊆m .	references	p	references × references
. ⊑ .	references	p	references × references
. ⊒ .	references	p	references × references
[]	references	c	references
{ . }	references	f	reference → referenceset
∅	references	c	referenceset
butlastn	references	f	nat × references → references
disj	references	p	references × references
dups	references	p	references
fillfirst	references	f	nat × reference × references → references
filter	references	f	references × references → references
firstn	references	f	nat × references → references
frome	references	f	references × reference → references
ins≤	references	f	reference × references → references
jvmref	reference	c	reference
lastn	references	f	nat × references → references
list2set	references	f	references → referenceset
m	nat-basic2	v	nat
merge	references	f	references × references → references
mklist	references	f	reference × nat → references
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
next	reference	f	reference → reference
ordered<	references	p	references
ordered≤	references	p	references
perm	references	p	references × references
pos	references	f	reference × references → nat
r	reference	v	reference
r0	reference	v	reference
r1	reference	v	reference
r2	reference	v	reference
reference	reference	s
references	references	s
referenceset	references	s
refs	references	v	references
refs0	references	v	references
refs1	references	v	references
refs10	references	v	references
refs2	references	v	references
refs3	references	v	references
refs4	references	v	references
refs5	references	v	references
refs6	references	v	references
refs7	references	v	references
refs8	references	v	references
refs9	references	v	references
restn	references	f	nat × references → references
rev	references	f	references → references
rmdup	references	f	references → references
rset	references	v	referenceset
rset0	references	v	referenceset
rset1	references	v	referenceset
rset2	references	v	referenceset
set2list	references	f	referenceset → references
sublist	references	f	nat × nat × references → references
this	reference	v	reference