[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
# .	array	f	array → nat
. % .	nat-div	f	nat × nat → nat
. % .	int-div	f	int × int → int
. * .	int-mult	f	int × int → int
. * .	nat-mult	f	nat × nat → nat
. + .	int-basic2	f	int × int → int
. + .	nat-basic2	f	nat × nat → nat
. +1	int-basic1	f	int → int
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. - .	int-abs	f	int × int → int
. -1	int-basic1	f	int → int
. -1	nat-basic1	f	nat → nat
. .data	ring-buffer	f	ring_buffer → array
. .data:= .	ring-buffer	f	ring_buffer × array → ring_buffer
. .first	ring-buffer	f	ring_buffer → int
. .first:= .	ring-buffer	f	ring_buffer × int → ring_buffer
. .len	ring-buffer	f	ring_buffer → int
. .len:= .	ring-buffer	f	ring_buffer × int → ring_buffer
. .size	ring-buffer	f	ring_buffer → int
. .size:= .	ring-buffer	f	ring_buffer × int → ring_buffer
. / .	int-div	f	int × int → int
. / .	nat-div	f	nat × nat → nat
. < .	nat-basic1	p	nat × nat
. < .	int-basic1	p	int × int
. > .	nat	p	nat × nat
. > .	int-abs	p	int × int
. [ . ]	array	f	array × nat → elem
. [ . ]	array	f	array × nat × elem → array
. ≤ .	nat	p	nat × nat
. ≤ .	int-abs	p	int × int
. ≥ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
~ .	int-abs	f	int → int
a	elem	v	elem
abs	int-abs	f	int → int
ar	array	v	array
ar0	array	v	array
ar1	array	v	array
ar2	array	v	array
array	array	s
b	elem	v	elem
buf	ring-buffer	v	ring_buffer
c	elem	v	elem
elem	elem	s
i	int-basic1	v	int
i→n	intnat	f	int → nat
i0	int-basic1	v	int
i1	ring-buffer	v	int
i2	ring-buffer	v	int
i3	ring-buffer	v	int
i4	ring-buffer	v	int
int	int-basic1	s
j	int-basic1	v	int
j0	int-basic1	v	int
m	nat-basic2	v	nat
mk	ring-buffer	f	array × int × int × int → ring_buffer
mkarray	array	f	nat → array
n	nat-basic1	v	nat
n→i	intnat	f	nat → int
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
pos	array	f	array × elem → nat
ring_buffer	ring-buffer	s