[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
#	queue	function, queue → nat
#	array	function, array → nat
#	list-data	function, list → nat
%	nat-div	function, nat × nat → nat
%	int-div	function, int × int → int
'	queue	function, elem → queue
'	list	function, elem → list
*	nat-mult	function, nat × nat → nat
*	int-mult	function, int × int → int
+	queue	function, elem × queue → queue
+	queue	function, queue × queue → queue
+	queue	function, elem × elem → queue
+	int-basic2	function, int × int → int
+	list	function, list × list → list
+	list	function, list × elem → list
+	list	function, elem × elem → list
+	list-data	function, elem × list → list
+	nat-basic2	function, nat × nat → nat
++	queue	function, queue × elem → queue
++	list-dup	function, list × elem → list
+1	int-basic1	function, int → int
+1	nat-basic1	function, nat → nat
-	int-abs	function, int × int → int
-	nat	function, nat × nat → nat
-1	int-basic1	function, int → int
-1	nat-basic1	function, nat → nat
-1l	list-del	function, list × elem → list
-1l	list-del	function, list × nat → list
-1l	queue	function, queue × elem → queue
-1l	queue	function, queue × nat → queue
-l	list-del	function, list × elem → list
-l	queue	function, queue × elem → queue
.butlast	queue	function, queue → queue
.butlast	list-last	function, list → list
.data	ring-buffer	function, ring_buffer → array
.data:=	ring-buffer	function, ring_buffer × array → ring_buffer
.first	ring-buffer	function, ring_buffer → int
.first	list-data	function, list → elem
.first:=	ring-buffer	function, ring_buffer × int → ring_buffer
.last	queue	function, queue → elem
.last	list-last	function, list → elem
.len	ring-buffer	function, ring_buffer → int
.len:=	ring-buffer	function, ring_buffer × int → ring_buffer
.rest	list-data	function, list → list
.size	ring-buffer	function, ring_buffer → int
.size:=	ring-buffer	function, ring_buffer × int → ring_buffer
/	nat-div	function, nat × nat → nat
/	int-div	function, int × int → int
<	queue	predicate, queue × queue
<	int-basic1	predicate, int × int
<	list-data	predicate, list × list
<	nat-basic1	predicate, nat × nat
>	int-abs	predicate, int × int
>	nat	predicate, nat × nat
[]	queue	constant, queue
[]	list-data	constant, list
]	list-del	function, list × nat → elem
]	list-del	function, list × nat × elem → list
]	queue	function, queue × nat → elem
]	queue	function, queue × nat × elem → queue
]	array	function, array × nat → elem
]	array	function, array × nat × elem → array
a	elem	variable, elem
a0	queue-impl	variable, elem
a0	list-data	variable, elem
abs	refinement	predicate, ring_buffer × queue
abs	int-abs	function, int → int
ar	array	variable, array
ar0	array	variable, array
ar1	array	variable, array
ar2	array	variable, array
array	array	sort,
assert#	queue-impl	procedure, bool :
b	elem	variable, elem
buf	ring-buffer	variable, ring_buffer
butlastn	queue	function, nat × queue → queue
butlastn	list-last	function, nat × list → list
bv	queue-impl	variable, bool
c	elem	variable, elem
clear#	queue-impl	procedure, : ring_buffer
create#	queue-impl	procedure, int : ring_buffer
disj	queue	predicate, queue × queue
disj	list-dup	predicate, list × list
dups	queue	predicate, queue
dups	list-dup	predicate, list
elem	elem	sort,
fillfirst	queue	function, nat × elem × queue → queue
fillfirst	list-last	function, nat × elem × list → list
firstn	list-del	function, nat × list → list
firstn	queue	function, nat × queue → queue
frome	list-del	function, list × elem → list
frome	queue	function, queue × elem → queue
get#	queue-impl	procedure, int × array : elem
head	queue	function, queue → elem
head#	queue-impl	procedure, ring_buffer : elem
i	int-basic1	variable, int
i0	int-basic1	variable, int
i1	ring-buffer	variable, int
i2	ring-buffer	variable, int
i3	ring-buffer	variable, int
i4	ring-buffer	variable, int
int	int-basic1	sort,
inv	ring-buffer-inv	predicate, ring_buffer
i→n	intnat	function, int → nat
j	int-basic1	variable, int
j0	int-basic1	variable, int
lastn	list-del	function, nat × list → list
lastn	queue	function, nat × queue → queue
list	list-data	sort,
m	nat-basic2	variable, nat
mk	ring-buffer	function, array × int × int × int → ring_buffer
mkarray	array	function, nat → array
mklist	queue	function, elem × nat → queue
mklist	list-last	function, elem × nat → list
n	nat-basic1	variable, nat
n0	nat-basic1	variable, nat
n1	nat-basic1	variable, nat
nat	nat-basic1	sort,
n→i	intnat	function, nat → int
pop	queue	function, queue → queue
pop#	queue-impl	procedure, : ring_buffer × elem
pos	list-del	function, elem × list → nat
pos	queue	function, elem × queue → nat
pos	array	function, array × elem → nat
push	queue	function, queue × elem → queue
push#	queue-impl	procedure, elem : ring_buffer
put#	queue-impl	procedure, int × elem : array
queue	queue	sort,
restn	list-del	function, nat × list → list
restn	queue	function, nat × queue → queue
rev	queue	function, queue → queue
rev	list-last	function, list → list
ring_buffer	ring-buffer	sort,
rmdup	queue	function, queue → queue
rmdup	list-dup	function, list → list
sublist	list-del	function, nat × nat × list → list
sublist	queue	function, nat × nat × queue → queue
test#	queue-impl	procedure, elem × elem × elem :
tolist	refinement	function, ring_buffer × nat → queue
x	queue	variable, queue
x	list-data	variable, list
x0	queue	variable, queue
x0	list-data	variable, list
x1	queue	variable, queue
x1	list-data	variable, list
x2	queue	variable, queue
x2	list-data	variable, list
y	queue	variable, queue
y	list-data	variable, list
y0	queue	variable, queue
y0	list-data	variable, list
y1	queue	variable, queue
y1	list-data	variable, list
y2	queue	variable, queue
y2	list-data	variable, list
z	queue	variable, queue
z	list-data	variable, list
z0	queue	variable, queue
z0	list-data	variable, list
z1	queue	variable, queue
z1	list-data	variable, list
z2	queue	variable, queue
z2	list-data	variable, list
~	int-abs	function, int → int
≤	int-abs	predicate, int × int
≤	nat	predicate, nat × nat
≥	int-abs	predicate, int × int
≥	nat	predicate, nat × nat
∈	queue	predicate, elem × queue
∈	list	predicate, elem × list
⊑	queue	predicate, queue × queue
⊑	list-last	predicate, list × list
⊒	queue	predicate, queue × queue
⊒	list-last	predicate, list × list