[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
#	buffer	function, buffer → nat
#	array	function, array → nat
#	store	function, store → nat
#	abstract-volume	function, abstract-volume → nat
#	abstract-volumes	function, abstract-volumes → nat
#	set-basic	function, set → nat
#	nat-set	function, nat-set → nat
#	avolume	function, avolume → nat
%	nat-div	partial function, nat × nat → nat
*	nat-mult	function, nat × nat → nat
+	buffer	function, buffer × buffer → buffer
+	array-splice	function, array × array → array
+	avolume	function, avolume × avolume → avolume
+	nat-basic	function, nat × nat → nat
++	set-basic	function, set × elem → set
++	nat-set	function, nat-set × nat → nat-set
+1	nat-basic	function, nat → nat
-	nat	partial function, nat × nat → nat
--	store	function, store × elem → store
--	abstract-volumes	function, abstract-volumes × volid → abstract-volumes
--	set-union	function, set × elem → set
--	nat-set	function, nat-set × nat → nat-set
-1	nat-basic	partial function, nat → nat
.butmax	oset	partial function, set → set
.butmax	nat-set	partial function, nat-set → nat-set
.butmin	oset	partial function, set → set
.butmin	nat-set	partial function, nat-set → nat-set
.data	leb	partial function, leb → buffer
.data	aleb	partial function, aleb → buffer
.data:=	leb	partial function, leb × buffer → leb
.data:=	aleb	partial function, aleb × buffer → aleb
.fill	leb	partial function, leb → nat
.fill:=	leb	partial function, leb × nat → leb
.mapped?	leb	predicate, leb
.mapped?	aleb	predicate, aleb
.max	oset	partial function, set → elem
.max	nat-set	partial function, nat-set → nat
.min	oset	partial function, set → elem
.min	nat-set	partial function, nat-set → nat
/	nat-div	partial function, nat × nat → nat
<	oelem	predicate, elem × elem
<	oset	predicate, set × elem
<	oset	predicate, elem × set
<	nat-set	predicate, nat-set × nat
<	nat-set	predicate, nat × nat-set
<	nat-basic	predicate, nat × nat
>	nat	predicate, nat × nat
AVOL	ebm-avol-asm	variable, avolume,flexible
AVOLS	ebm-asm	variable, abstract-volumes,flexible
AVOLS0	ebm-asm	variable, abstract-volumes,flexible
BUF	ebm-avol-asm	variable, buffer,flexible
BUF	ebm-asm	variable, buffer,flexible
BUF0	ebm-avol-asm	variable, buffer,flexible
BUF0	ebm-asm	variable, buffer,flexible
EACCESS	error	constant, error
EBADFD	error	constant, error
EB_PAGE_SIZE	eraseblock	constant, nat
ECOMMIT	error	constant, error
EEXISTS	error	constant, error
EFAIL	error	constant, error
EINVAL	error	constant, error
EIO	error	constant, error
EISDIR	error	constant, error
ENOENT	error	constant, error
ENOMEM	error	constant, error
ENOSPC	error	constant, error
ENOTDIR	error	constant, error
ENOTEMPTY	error	constant, error
EROFS	error	constant, error
ERR	error-class	variable, error,flexible
ERR0	error-class	variable, error,flexible
ESUCCESS	error	constant, error
EUCLEAN	error	constant, error
LEB_SIZE	eraseblock	constant, nat
LNUM	ebm-avol-asm	variable, nat,flexible
LNUM	ebm-asm	variable, nat,flexible
N	ebm-avol-asm	variable, nat,flexible
N	ebm-asm	variable, nat,flexible
N0	ebm-avol-asm	variable, nat,flexible
N0	ebm-asm	variable, nat,flexible
N1	ebm-avol-asm	variable, nat,flexible
N1	ebm-asm	variable, nat,flexible
OFFSET	ebm-avol-asm	variable, nat,flexible
OFFSET	ebm-asm	variable, nat,flexible
PAGES_PER_LEB	eraseblock	constant, nat
PAGES_PER_PEB	eraseblock	constant, nat
PEB_SIZE	eraseblock	constant, nat
VOLID	ebm-asm	variable, volid,flexible
VOLID0	ebm-asm	variable, volid,flexible
VOLSIZE	ebm-vol-asm	variable, nat,flexible
VOLSIZE	ebm-avol-asm	variable, nat,flexible
\	set-union	function, set × set → set
\	nat-set	function, nat-set × nat-set → nat-set
]	buffer	partial function, buffer × nat × data → buffer
]	buffer	partial function, buffer × nat → data
]	array	partial function, array × nat × elem → array
]	array	partial function, array × nat → elem
]	store	partial function, store × elem → data
]	store	function, store × elem × data → store
]	abstract-volume	partial function, abstract-volume × nat × leb → abstract-volume
]	abstract-volume	partial function, abstract-volume × nat → leb
]	abstract-volumes	partial function, abstract-volumes × volid → abstract-volume
]	abstract-volumes	function, abstract-volumes × volid × abstract-volume → abstract-volumes
]	avolume	partial function, avolume × nat × aleb → avolume
]	avolume	partial function, avolume × nat → aleb
a	elem	variable, elem
abs	ebm-vol-abs	function, abstract-volume → avolume
abs	ebm-vol-abs	function, leb → aleb
abstract-volume	abstract-volume	sort,
abstract-volumes	abstract-volumes	sort,
aleb	aleb	variable, aleb
aleb	aleb	sort,
aleb0	avolume	variable, aleb
aleb1	avolume	variable, aleb
align↑	align	function, nat × nat → nat
align↓	align	function, nat × nat → nat
ar	array	variable, array
ar0	array	variable, array
ar1	array	variable, array
ar2	array	variable, array
array	array	sort,
avol	avolume	variable, avolume
avol0	avolume	variable, avolume
avol1	avolume	variable, avolume
avol2	avolume	variable, avolume
avols	abstract-volumes	variable, abstract-volumes
avols0	abstract-volumes	variable, abstract-volumes
avols1	abstract-volumes	variable, abstract-volumes
avols2	abstract-volumes	variable, abstract-volumes
avolume	avolume	sort,
b	elem	variable, elem
buf	buffer	variable, buffer
buf0	buffer	variable, buffer
buf1	buffer	variable, buffer
buf2	buffer	variable, buffer
buffer	buffer	sort,
c	elem	variable, elem
cmp	buffer	partial predicate, buffer × data × nat × nat
cmp	buffer	partial predicate, buffer × nat × buffer × nat × nat
cmp	array-copy	partial predicate, array × elem × nat × nat
cmp	array-copy	partial predicate, array × nat × array × nat × nat
cmp	abstract-volume	partial predicate, abstract-volume × leb × nat × nat
cmp	abstract-volume	partial predicate, abstract-volume × nat × abstract-volume × nat × nat
cmp	avolume	partial predicate, avolume × aleb × nat × nat
cmp	avolume	partial predicate, avolume × nat × avolume × nat × nat
copy	buffer	partial function, buffer × nat × buffer × nat × nat → buffer
copy	array-copy	partial function, array × nat × array × nat × nat → array
copy	abstract-volume	partial function, abstract-volume × nat × abstract-volume × nat × nat → abstract-volume
copy	avolume	partial function, avolume × nat × avolume × nat × nat → avolume
d	data	variable, data
d0	data	variable, data
d1	data	variable, data
d2	data	variable, data
data	data	sort,
default-volid	default-volid	constant, volid
ebm-cons	ebm-base	predicate, abstract-volume
ebm-cons	ebm-base	predicate, abstract-volumes
ebm-initial	ebm-base	predicate, abstract-volumes
ebm-vol-inv	ebm-vol-inv	predicate, avolume
ebm_avol_change#	ebm-avol-asm	procedure, nat × nat × buffer : avolume : error
ebm_avol_format#	ebm-avol-asm	procedure, nat : : avolume × error
ebm_avol_get_leb_size#	ebm-avol-asm	procedure, avolume : : nat
ebm_avol_get_page_size#	ebm-avol-asm	procedure, avolume : : nat
ebm_avol_get_volume_size#	ebm-avol-asm	procedure, avolume : : nat
ebm_avol_read#	ebm-avol-asm	procedure, nat × nat × nat × nat × avolume : buffer : error
ebm_avol_recover#	ebm-avol-asm	procedure, : avolume : error
ebm_avol_remap#	ebm-avol-asm	procedure, nat : avolume : error
ebm_avol_sync_device#	ebm-avol-asm	procedure, avolume : : error
ebm_avol_unmap#	ebm-avol-asm	procedure, nat : avolume
ebm_avol_write#	ebm-avol-asm	procedure, nat × nat × nat × nat × buffer : avolume : error
ebm_change#	ebm-asm	procedure, volid × nat × nat × buffer : abstract-volumes : error
ebm_create_volume#	ebm-asm	procedure, volid × nat : abstract-volumes : error
ebm_erase#	ebm-asm	procedure, volid × nat : abstract-volumes : error
ebm_format#	ebm-asm	procedure, : : abstract-volumes × error
ebm_get_leb_size#	ebm-asm	procedure, abstract-volumes : : nat
ebm_get_page_size#	ebm-asm	procedure, abstract-volumes : : nat
ebm_get_volume_size#	ebm-asm	procedure, volid × abstract-volumes : : nat
ebm_map#	ebm-asm	procedure, volid × nat : abstract-volumes : error
ebm_read#	ebm-asm	procedure, volid × nat × nat × nat × nat × abstract-volumes : buffer : error
ebm_recover#	ebm-asm	procedure, : abstract-volumes : error
ebm_sync_device#	ebm-asm	procedure, abstract-volumes : : error
ebm_unmap#	ebm-asm	procedure, volid × nat : abstract-volumes
ebm_vol_change#	ebm-vol-asm	procedure, nat × nat × buffer × volid : abstract-volumes : error
ebm_vol_format#	ebm-vol-asm	procedure, nat : volid × abstract-volumes : error
ebm_vol_get_leb_size#	ebm-vol-asm	procedure, abstract-volumes : : nat
ebm_vol_get_page_size#	ebm-vol-asm	procedure, abstract-volumes : : nat
ebm_vol_get_volume_size#	ebm-vol-asm	procedure, volid × abstract-volumes : : nat
ebm_vol_read#	ebm-vol-asm	procedure, nat × nat × nat × nat × volid × abstract-volumes : buffer : error
ebm_vol_recover#	ebm-vol-asm	procedure, : abstract-volumes : volid × error
ebm_vol_remap#	ebm-vol-asm	procedure, nat × volid : abstract-volumes : error
ebm_vol_sync_device#	ebm-vol-asm	procedure, abstract-volumes : : error
ebm_vol_unmap#	ebm-vol-asm	procedure, nat × volid : abstract-volumes
ebm_vol_write#	ebm-vol-asm	procedure, nat × nat × nat × nat × buffer × volid : abstract-volumes : error
ebm_write#	ebm-asm	procedure, volid × nat × nat × nat × nat × buffer : abstract-volumes : error
elem	elem	sort,
empty	buffer	constant, data
empty	array-splice	constant, elem
empty	avolume	constant, aleb
emptyleb	eraseblock	constant, buffer
emptypage	eraseblock	constant, buffer
emptypeb	eraseblock	constant, buffer
erased	leb	constant, leb
err	error	variable, error
err0	error	variable, error
err1	error	variable, error
error	error	sort,
evol	abstract-volume	variable, abstract-volume
evol0	abstract-volume	variable, abstract-volume
evol1	abstract-volume	variable, abstract-volume
evol2	abstract-volume	variable, abstract-volume
fail#	error-class	procedure, : : error
fail_or_success#	error-class	procedure, : : error
fill	buffer	partial function, buffer × data × nat × nat → buffer
fill	buffer	function, buffer × data → buffer
fill	array-copy	partial function, array × elem × nat × nat → array
fill	array-copy	function, array × elem → array
fill	abstract-volume	partial function, abstract-volume × leb × nat × nat → abstract-volume
fill	abstract-volume	function, abstract-volume × leb → abstract-volume
fill	avolume	partial function, avolume × aleb × nat × nat → avolume
fill	avolume	function, avolume × aleb → avolume
idrange	buffer	partial predicate, buffer × nat × nat
idrange	array-copy	partial predicate, array × nat × nat
idrange	abstract-volume	partial predicate, abstract-volume × nat × nat
idrange	avolume	partial predicate, avolume × nat × nat
id○	buffer	predicate, buffer × buffer × nat
id○	array-copy	predicate, array × array × nat
id○	abstract-volume	predicate, abstract-volume × abstract-volume × nat
id○	avolume	predicate, avolume × avolume × nat
is-aligned	align	predicate, nat × nat
isempty	eraseblock	predicate, buffer × nat × nat
isempty	eraseblock	predicate, buffer
leb	leb	variable, leb
leb	leb	sort,
leb0	abstract-volume	variable, leb
leb1	abstract-volume	variable, leb
m	nat-basic	variable, nat
m0	array-copy	variable, nat
mapped	leb	function, buffer × nat → leb
mapped	aleb	function, buffer → aleb
max	min-max	function, nat × nat → nat
min	min-max	function, nat × nat → nat
mkabstractvolume	abstract-volume	function, nat → abstract-volume
mkarray	array	function, nat → array
mkavolume	avolume	function, nat → avolume
mkbuf	buffer	function, nat → buffer
mkemparray	array-splice	function, nat → array
mkemparray	avolume	function, nat → avolume
mkempbuf	buffer	function, nat → buffer
mkzarray	array-splice	function, nat → array
mkzarray	avolume	function, nat → avolume
mkzbuf	buffer	function, nat → buffer
n	nat-basic	variable, nat
n0	nat-basic	variable, nat
n1	nat-basic	variable, nat
n2	nat-set	variable, nat
n3	nat-set	variable, nat
n4	nat-set	variable, nat
nat	nat-basic	sort,
nat-set	nat-set	sort,
ns	nat-set	variable, nat-set
ns0	nat-set	variable, nat-set
ns1	nat-set	variable, nat-set
ns2	nat-set	variable, nat-set
range=	buffer	predicate, buffer × nat × buffer × nat × nat
range=	array-splice	predicate, array × nat × array × nat × nat
range=	avolume	predicate, avolume × nat × avolume × nat × nat
resize	buffer	function, buffer × nat → buffer
resize	array-splice	function, array × nat → array
resize	avolume	function, avolume × nat → avolume
rev	buffer	partial function, buffer × nat → buffer
rev	buffer	function, buffer → buffer
rev	array-copy	partial function, array × nat → array
rev	array-copy	function, array → array
rev	abstract-volume	partial function, abstract-volume × nat → abstract-volume
rev	abstract-volume	function, abstract-volume → abstract-volume
rev	avolume	partial function, avolume × nat → avolume
rev	avolume	function, avolume → avolume
s	set-basic	variable, set
s0	set-basic	variable, set
s1	set-basic	variable, set
s2	set-basic	variable, set
set	set-basic	sort,
splice	buffer	function, buffer × nat × buffer × nat × nat → buffer
splice	array-splice	function, array × nat × array × nat × nat → array
splice	avolume	function, avolume × nat × avolume × nat × nat → avolume
st	store	variable, store
st0	store	variable, store
st1	store	variable, store
st2	store	variable, store
store	store	sort,
subarray	buffer	partial function, buffer × nat × nat → buffer
subarray	array-copy	partial function, array × nat × nat → array
subarray	abstract-volume	partial function, abstract-volume × nat × nat → abstract-volume
subarray	avolume	partial function, avolume × nat × nat → avolume
subseteq	abstract-volumes	predicate, abstract-volumes × abstract-volumes
unmapped	leb	constant, leb
unmapped	aleb	constant, aleb
v	volid	variable, volid
v0	volid	variable, volid
v1	volid	variable, volid
v2	volid	variable, volid
valid-leb	ebm-base	predicate, leb
volid	volid	sort,
zero	buffer	constant, data
zero	array-splice	constant, elem
zero	avolume	constant, aleb
}	set-union	function, elem → set
}	nat-set	function, nat → nat-set
∅	store	constant, store
∅	abstract-volumes	constant, abstract-volumes
∅	set-basic	constant, set
∅	nat-set	constant, nat-set
∈	buffer	predicate, data × buffer
∈	array-copy	predicate, elem × array
∈	store	predicate, elem × store
∈	abstract-volume	predicate, leb × abstract-volume
∈	abstract-volumes	predicate, volid × abstract-volumes
∈	set-basic	predicate, elem × set
∈	nat-set	predicate, nat × nat-set
∈	avolume	predicate, aleb × avolume
∩	set-union	function, set × set → set
∩	nat-set	function, nat-set × nat-set → nat-set
∪	set-union	function, set × set → set
∪	nat-set	function, nat-set × nat-set → nat-set
≤	nat	predicate, nat × nat
≥	nat	predicate, nat × nat
⊆	store	predicate, store × store
⊆	ebm-base	predicate, abstract-volumes × abstract-volumes
⊆	set-basic	predicate, set × set
⊆	nat-set	predicate, nat-set × nat-set
⊆	ebm-vol-inv	predicate, avolume × avolume
⌋	error-class	predicate, error