[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
# .	file-data-store	f	fidset → nat
# .	file-data-store	f	file-data-store → nat
# .	buffer	f	buffer → nat
. + .	nat-basic	f	nat × nat → nat
. + .	buffer	f	buffer × buffer → buffer
. ++ .	file-data-store	f	fidset × fid → fidset
. +1	nat-basic	f	nat → nat
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	file-data-store	f	file-data-store × fid → file-data-store
. -- .	file-data-store	f	fidset × fid → fidset
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. .content	file-data	f	file-data → buffer
. .content:= .	file-data	f	file-data × buffer → file-data
. .meta	file-data	f	file-data → metadata
. .meta:= .	file-data	f	file-data × metadata → file-data
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	file-data-store	pf	file-data-store × fid → file-data with λ fs, fid. fid ∈ fs
. [ . ]	buffer	pf	buffer × nat × data → buffer with λ buf, n, d. n < # buf
. [ . ]	file-data-store	f	file-data-store × fid × file-data → file-data-store
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. \ .	file-data-store	f	fidset × fidset → fidset
. \ .	file-data-store	f	file-data-store × fidset → file-data-store
. \| .	file-data-store	f	file-data-store × fidset → file-data-store
. ∈ .	file-data-store	p	file-data × file-data-store
. ∈ .	file-data-store	p	fid × fidset
. ∈ .	file-data-store	p	fid × file-data-store
. ∈ .	buffer	p	data × buffer
. ∩ .	file-data-store	f	fidset × fidset → fidset
. ∪ .	file-data-store	f	fidset × fidset → fidset
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	file-data-store	p	fidset × fidset
. ⊆ .	file-data-store	p	file-data-store × file-data-store
. ⊕ .	file-data-store	f	file-data-store × file-data-store → file-data-store
{ . }	file-data-store	f	fid → fidset
∅	file-data-store	c	file-data-store
∅	file-data-store	c	fidset
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
cmp	buffer	pp	buffer × data × nat × nat with λ buf, d, m, n. m + n ≤ # buf
cmp	buffer	pp	buffer × nat × buffer × nat × nat with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0
copy	buffer	pf	buffer × nat × buffer × nat × nat → buffer with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
dom .	file-data-store	f	file-data-store → fidset
empty	buffer	c	data
f	file-data	v	file-data
f0	file-data-store	v	file-data
f1	file-data-store	v	file-data
f2	file-data-store	v	file-data
fid	file-id	s
fid	file-id	v	fid
fid1	file-data-store	v	fid
fid2	file-data-store	v	fid
fids	file-data-store	v	fidset
fids0	file-data-store	v	fidset
fids1	file-data-store	v	fidset
fids2	file-data-store	v	fidset
fidset	file-data-store	s
file-data	file-data	s
file-data-store	file-data-store	s
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fill	buffer	f	buffer × data → buffer
fs	file-data-store	v	file-data-store
fs0	file-data-store	v	file-data-store
fs1	file-data-store	v	file-data-store
fs2	file-data-store	v	file-data-store
id○	buffer	p	buffer × buffer × nat
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
m	nat-basic	v	nat
m0	array-copy	v	nat
max	min-max	f	nat × nat → nat
md	metadata	v	metadata
md0	file-data	v	metadata
metadata	metadata	s
min	min-max	f	nat × nat → nat
mkbuf	buffer	f	nat → buffer
mkempbuf	buffer	f	nat → buffer
mkfile	file-data	f	metadata × buffer → file-data
mkzbuf	buffer	f	nat → buffer
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	buffer	f	buffer → buffer
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
zero	buffer	c	data