[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
# .	open-files	f	nat-set → nat
# .	open-files	f	open-files → nat
. + .	nat-basic	f	nat × nat → nat
. ++ .	open-files	f	nat-set × nat → nat-set
. +1	nat-basic	f	nat → nat
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	open-files	f	open-files × nat → open-files
. -- .	open-files	f	nat-set × nat → nat-set
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. .ino	file	f	file → nat
. .ino:= .	file	f	file × nat → file
. .mode	file	f	file → file-mode
. .mode:= .	file	f	file × file-mode → file
. .pos	file	f	file → nat
. .pos:= .	file	f	file × nat → file
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	open-files	pf	open-files × nat → file with λ of, fd. fd ∈ of
. [ . ]	open-files	f	open-files × nat × file → open-files
. \ .	open-files	f	nat-set × nat-set → nat-set
. \ .	open-files	f	open-files × nat-set → open-files
. \| .	open-files	f	open-files × nat-set → open-files
. ∈ .	open-files	p	file × open-files
. ∈ .	open-files	p	nat × nat-set
. ∈ .	open-files	p	nat × open-files
. ∩ .	open-files	f	nat-set × nat-set → nat-set
. ∪ .	open-files	f	nat-set × nat-set → nat-set
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	open-files	p	nat-set × nat-set
. ⊆ .	open-files	p	open-files × open-files
. ⊕ .	open-files	f	open-files × open-files → open-files
{ . }	open-files	f	nat → nat-set
∅	open-files	c	open-files
∅	open-files	c	nat-set
MODE_R	file-mode	c	file-mode
MODE_RW	file-mode	c	file-mode
MODE_W	file-mode	c	file-mode
dom .	open-files	f	open-files → nat-set
fd	open-files	v	nat
fd1	open-files	v	nat
fd2	open-files	v	nat
file	file	s
file	file	v	file
file-mode	file-mode	s
file0	open-files	v	file
file1	open-files	v	file
file2	open-files	v	file
m	nat-basic	v	nat
m0	file	v	nat
m1	file	v	nat
m2	file	v	nat
mkfile	file	f	nat × file-mode × nat → file
mode	file-mode	v	file-mode
mode0	file	v	file-mode
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
nat-set	open-files	s
ns	open-files	v	nat-set
ns0	open-files	v	nat-set
ns1	open-files	v	nat-set
ns2	open-files	v	nat-set
of	open-files	v	open-files
of0	open-files	v	open-files
of1	open-files	v	open-files
of2	open-files	v	open-files
open-files	open-files	s