| symbol | specification | entry |
|---|
| # | buffer | function,
buffer → nat |
| # | array | function,
array → nat |
| # | set-basic | function,
set → nat |
| # | nat-set | function,
nat-set → nat |
| # | list-data | function,
list → nat |
| # | nat-list-set | function,
nat-set → nat |
| # | nat-list-set | function,
nat-list → nat |
| # | lp-array | function,
lp-array → nat |
| # | avolume | function,
avolume → nat |
| % | nat-div | partial function,
nat × nat → nat |
| ' | list | function,
elem → list |
| ' | nat-list-set | function,
nat → nat-list |
| * | nat-mult | function,
nat × nat → nat |
| + | buffer | function,
buffer × buffer → buffer |
| + | array-splice | function,
array × array → array |
| + | list-data | function,
elem × list → list |
| + | list | function,
list × elem → list |
| + | list | function,
list × list → list |
| + | nat-list-set | function,
nat-list × nat → nat-list |
| + | nat-list-set | function,
nat-list × nat-list → nat-list |
| + | nat-list-set | function,
nat × nat-list → nat-list |
| + | 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 |
| ++ | list-dup | function,
list × elem → list |
| ++ | nat-list-set | function,
nat-set × nat → nat-set |
| ++ | nat-list-set | function,
nat-list × nat → nat-list |
| +1 | nat-basic | function,
nat → nat |
| +2 | list | function,
elem × elem → list |
| +2 | nat-list-set | function,
nat × nat → nat-list |
| - | nat | partial function,
nat × nat → nat |
| -- | set-union | function,
set × elem → set |
| -- | nat-set | function,
nat-set × nat → nat-set |
| -- | nat-list-set | function,
nat-set × nat → nat-set |
| -1 | nat-basic | partial function,
nat → nat |
| -1l | list-del | function,
list × elem → list |
| -1l | nat-list-set | function,
nat-list × nat → nat-list |
| -l | list-del | function,
list × elem → list |
| -l | nat-list-set | function,
nat-list × nat → nat-list |
| -p | list-del | function,
list × nat → list |
| -p | nat-list-set | function,
nat-list × nat → nat-list |
| .align↓ | awbuf-inv | function,
avolume → avolume |
| .align↓ | awbuf-inv | function,
buffer → buffer |
| .butlast | list-last | partial function,
list → list |
| .butlast | nat-list-set | partial function,
nat-list → nat-list |
| .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 |
| .content | wbuf | function,
wbuf → buffer |
| .content:= | wbuf | function,
wbuf × buffer → wbuf |
| .data | aleb | partial function,
aleb → buffer |
| .data:= | aleb | partial function,
aleb × buffer → aleb |
| .filter | array-indices | function,
nat-set × nat → bool → nat-set |
| .flags | lprops | function,
lprops → lpropflags |
| .flags:= | lprops | function,
lprops × lpropflags → lprops |
| .gcheapidx | lprops | function,
lprops → nat |
| .gcheapidx:= | lprops | function,
lprops × nat → lprops |
| .head | list-data | partial function,
list → elem |
| .head | nat-list-set | partial function,
nat-list → nat |
| .indicesWhere | array-indices | function,
array × elem → bool × nat → nat-list |
| .indicesWhere | array-indices | function,
array × elem → bool → nat-list |
| .indicesWhere | lp-array | function,
lp-array × lprops → bool × nat → nat-list |
| .indicesWhere | lp-array | function,
lp-array × lprops → bool → nat-list |
| .isbuf? | bufleb | predicate,
bufleb |
| .last | list-last | partial function,
list → elem |
| .last | nat-list-set | partial function,
nat-list → nat |
| .leb | bufleb | partial function,
bufleb → nat |
| .map | array-indices | function,
array × elem → elem → array |
| .map | array-indices | function,
nat-set × nat → nat → nat-set |
| .map | lp-array | function,
lp-array × lprops → lprops → lp-array |
| .mapIf | array-indices | function,
array × elem → bool × elem → elem × nat → array |
| .mapIf | array-indices | function,
array × elem → bool × elem → elem → array |
| .mapIf | lp-array | function,
lp-array × lprops → bool × lprops → lprops × nat → lp-array |
| .mapIf | lp-array | function,
lp-array × lprops → bool × lprops → lprops → lp-array |
| .mapIndices | array-indices | function,
array × nat-set × elem → elem → array |
| .mapIndices | array-indices | function,
array × nat-list × elem → elem → array |
| .mapIndices | lp-array | function,
lp-array × nat-set × lprops → lprops → lp-array |
| .mapIndices | lp-array | function,
lp-array × nat-list × lprops → lprops → lp-array |
| .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 |
| .nbytes | wbuf | function,
wbuf → nat |
| .nbytes:= | wbuf | function,
wbuf × nat → wbuf |
| .offset | wbuf | function,
wbuf → nat |
| .offset:= | wbuf | function,
wbuf × nat → wbuf |
| .ref-size | lprops | function,
lprops → nat |
| .ref-size:= | lprops | function,
lprops × nat → lprops |
| .size | lprops | function,
lprops → nat |
| .size:= | lprops | function,
lprops × nat → lprops |
| .tail | list-data | partial function,
list → list |
| .tail | nat-list-set | partial function,
nat-list → nat-list |
| .toSet | list+set | function,
list → set |
| .toSet | nat-list-set | function,
nat-list → nat-set |
| / | 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 |
| < | list-data | predicate,
list × list |
| < | nat-list-set | predicate,
nat-list × nat-list |
| < | nat-list-less | predicate,
nat-list × nat |
| < | nat-basic | predicate,
nat × nat |
| > | nat | predicate,
nat × nat |
| AROFS | awbuf-asm | variable,
bool,flexible |
| AROFS0 | awbuf-asm | variable,
bool,flexible |
| BEGINBUF | wbuf-asm | variable,
nat,flexible |
| BEGINWBUF | wbuf-asm | variable,
nat,flexible |
| BUF | awbuf-asm | variable,
buffer,flexible |
| BUF | apersistence-io-asm | variable,
buffer,flexible |
| BUF0 | awbuf-asm | variable,
buffer,flexible |
| BUF0 | apersistence-io-asm | variable,
buffer,flexible |
| BUFLEB | wbuf-asm | variable,
bufleb,flexible |
| BUFLEB0 | wbuf-asm | variable,
bufleb,flexible |
| COMMIT? | awbuf-asm | variable,
bool,flexible |
| COMMIT? | apersistence-io-asm | variable,
bool,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 |
| ISBUF | awbuf-asm | variable,
bool,flexible |
| ISBUF | apersistence-io-asm | variable,
bool,flexible |
| LEB_SIZE | eraseblock | constant,
nat |
| LNUM | awbuf-asm | variable,
nat,flexible |
| LNUM | apersistence-io-asm | variable,
nat,flexible |
| LOG | awbuf-asm | variable,
nat-list,flexible |
| LOG | apersistence-io-asm | variable,
nat-list,flexible |
| LPT | awbuf-asm | variable,
lp-array,flexible |
| LPT | apersistence-io-asm | variable,
lp-array,flexible |
| LP_FREE | lprops | constant,
lpropflags |
| LP_GROUP_NODES | lprops | constant,
lpropflags |
| LP_INDEX_NODES | lprops | constant,
lpropflags |
| N | awbuf-asm | variable,
nat,flexible |
| N | apersistence-io-asm | variable,
nat,flexible |
| N0 | awbuf-asm | variable,
nat,flexible |
| N0 | apersistence-io-asm | variable,
nat,flexible |
| N1 | awbuf-asm | variable,
nat,flexible |
| N1 | apersistence-io-asm | variable,
nat,flexible |
| N2 | wbuf-asm | variable,
nat,flexible |
| OFFSET | awbuf-asm | variable,
nat,flexible |
| OFFSET | apersistence-io-asm | variable,
nat,flexible |
| ORPHANS | awbuf-asm | variable,
nat-set,flexible |
| ORPHANS | apersistence-io-asm | variable,
nat-set,flexible |
| PAGESIZE | wbuf-asm | variable,
nat,flexible |
| PAGES_PER_LEB | eraseblock | constant,
nat |
| PAGES_PER_PEB | eraseblock | constant,
nat |
| PEB_SIZE | eraseblock | constant,
nat |
| PLOG | apersistence-io-asm | variable,
nat-list,flexible |
| PLPT | apersistence-io-asm | variable,
lp-array,flexible |
| PMAXINO | apersistence-io-asm | variable,
nat,flexible |
| PMAXINO0 | apersistence-io-asm | variable,
nat,flexible |
| PORPHANS | apersistence-io-asm | variable,
nat-set,flexible |
| PROOTADR | apersistence-io-asm | variable,
address,flexible |
| PROOTADR0 | apersistence-io-asm | variable,
address,flexible |
| PVOL | apersistence-io-asm | variable,
avolume,flexible |
| ROFS | wbuf-asm | variable,
bool,flexible |
| ROFS0 | wbuf-asm | variable,
bool,flexible |
| SIZE | awbuf-asm | variable,
nat,flexible |
| SIZE | apersistence-io-asm | variable,
nat,flexible |
| VOLSIZE | awbuf-asm | variable,
nat,flexible |
| VOLSIZE | apersistence-io-asm | variable,
nat,flexible |
| WBUF | wbuf-asm | variable,
wbuf,flexible |
| WBUFLEB | awbuf-asm | variable,
bufleb,flexible |
| WBUFLEB0 | awbuf-asm | variable,
bufleb,flexible |
| WLOG | wbuf-asm | variable,
nat-list,flexible |
| WLOG | awbuf-asm | variable,
nat-list,flexible |
| WLPT | wbuf-asm | variable,
lp-array,flexible |
| WLPT | awbuf-asm | variable,
lp-array,flexible |
| WMAXINO | wbuf-asm | variable,
nat,flexible |
| WMAXINO | awbuf-asm | variable,
nat,flexible |
| WMAXINO0 | awbuf-asm | variable,
nat,flexible |
| WORPHANS | wbuf-asm | variable,
nat-set,flexible |
| WORPHANS | awbuf-asm | variable,
nat-set,flexible |
| WROOTADR | wbuf-asm | variable,
address,flexible |
| WROOTADR | awbuf-asm | variable,
address,flexible |
| WROOTADR0 | awbuf-asm | variable,
address,flexible |
| WVOL | wbuf-asm | variable,
avolume,flexible |
| WVOL | awbuf-asm | variable,
avolume,flexible |
| [] | list-data | constant,
list |
| [] | nat-list-set | constant,
nat-list |
| \ | set-union | function,
set × set → set |
| \ | nat-set | function,
nat-set × nat-set → nat-set |
| \ | nat-list-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 |
| ] | list-del | partial function,
list × nat × elem → list |
| ] | list-del | partial function,
list × nat → elem |
| ] | nat-list-set | partial function,
nat-list × nat × nat → nat-list |
| ] | nat-list-set | partial function,
nat-list × nat → nat |
| ] | lp-array | partial function,
lp-array × nat × lprops → lp-array |
| ] | lp-array | partial function,
lp-array × nat → lprops |
| ] | avolume | partial function,
avolume × nat × aleb → avolume |
| ] | avolume | partial function,
avolume × nat → aleb |
| a | elem | variable,
elem |
| a0 | list-data | variable,
elem |
| abs | wbuf-abs | predicate,
avolume × bufleb × wbuf × avolume × bool |
| abs⊕ | wbuf-abs | function,
aleb × wbuf → aleb |
| address | address | sort,
|
| adr | address | variable,
address |
| adr0 | address | variable,
address |
| adr1 | address | variable,
address |
| adr2 | address | variable,
address |
| adr3 | address | variable,
address |
| adr4 | address | variable,
address |
| adr5 | address | variable,
address |
| 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 |
| apersistence_io_add_log_leb# | apersistence-io-asm | procedure,
nat × address × nat × avolume × lp-array × nat-set : nat-list : error |
| apersistence_io_commit# | apersistence-io-asm | procedure,
lp-array × address × nat × avolume
: nat-set × address × nat × nat-list × lp-array × nat-set
: error |
| apersistence_io_format# | apersistence-io-asm | procedure,
nat × nat × lp-array × address × nat
:
: address × nat × nat-list × avolume × lp-array × nat-set × error |
| apersistence_io_get_leb_size# | apersistence-io-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set : : nat |
| apersistence_io_get_page_size# | apersistence-io-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set : : nat |
| apersistence_io_get_volume_size# | apersistence-io-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set : : nat |
| apersistence_io_read# | apersistence-io-asm | procedure,
nat × nat × nat × nat × address × nat × nat-list × avolume × lp-array ×
nat-set
: buffer
: error |
| apersistence_io_recover# | apersistence-io-asm | procedure,
: address × nat × nat-set × nat-list × lp-array × address × nat ×
nat-list × lp-array × nat-set × avolume
: error |
| apersistence_io_remap# | apersistence-io-asm | procedure,
nat × address × nat × nat-list × lp-array × nat-set : avolume : error |
| apersistence_io_requires_commit# | apersistence-io-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set : : bool |
| apersistence_io_unmap# | apersistence-io-asm | procedure,
nat × address × nat × nat-list × lp-array × nat-set : avolume |
| apersistence_io_write# | apersistence-io-asm | procedure,
nat × nat × nat × nat × buffer × address × nat × nat-list × lp-array ×
nat-set
: avolume
: error |
| 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 |
| avolume | avolume | sort,
|
| awbuf-inv | awbuf-inv | predicate,
avolume × bufleb |
| awbuf_add_log_leb# | awbuf-asm | procedure,
nat × nat × address × nat × avolume × lp-array × nat-set × bool
: nat-list × bufleb
: error |
| awbuf_commit# | awbuf-asm | procedure,
lp-array × address × nat × avolume × bufleb
: nat-set × address × nat × nat-list × lp-array × nat-set × bool
: error |
| awbuf_destroy_buf# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bool
: bufleb
: error |
| awbuf_enter_readonly# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb
:
: bool |
| awbuf_format# | awbuf-asm | procedure,
nat × nat × lp-array × address × nat
:
: address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool × error |
| awbuf_get_buf# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: bufleb |
| awbuf_get_leb_size# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: nat |
| awbuf_get_page_size# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: nat |
| awbuf_get_volume_size# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: nat |
| awbuf_is_readonly# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: bool |
| awbuf_move_buf# | awbuf-asm | procedure,
nat × nat × address × nat × nat-list × avolume × lp-array × nat-set ×
bool
: bufleb
: error |
| awbuf_read_buf# | awbuf-asm | procedure,
nat × nat × nat × address × nat × nat-list × avolume × lp-array ×
nat-set × bufleb × bool
: buffer
: error |
| awbuf_recover# | awbuf-asm | procedure,
: address × nat × nat-set × nat-list × lp-array × address × nat ×
nat-list × lp-array × nat-set × avolume
: bufleb × bool × error |
| awbuf_remap# | awbuf-asm | procedure,
nat × address × nat × nat-list × lp-array × nat-set × bufleb × bool
: avolume
: error |
| awbuf_requires_commit# | awbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set × bufleb ×
bool
:
: bool |
| awbuf_unmap# | awbuf-asm | procedure,
nat × address × nat × nat-list × lp-array × nat-set × bufleb × bool
: avolume |
| awbuf_write_buf# | awbuf-asm | procedure,
nat × buffer × address × nat × nat-list × lp-array × nat-set × bufleb
: avolume × bool
: error |
| b | elem | variable,
elem |
| bleb | bufleb | variable,
bufleb |
| buf | buffer | variable,
buffer |
| buf0 | buffer | variable,
buffer |
| buf1 | buffer | variable,
buffer |
| buf2 | buffer | variable,
buffer |
| buffer | buffer | sort,
|
| buffered | bufleb | function,
nat → bufleb |
| bufleb | bufleb | sort,
|
| butlastn | list-last | partial function,
nat × list → list |
| butlastn | nat-list-set | partial function,
nat × nat-list → nat-list |
| 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 | lp-array | partial predicate,
lp-array × lprops × nat × nat |
| cmp | lp-array | partial predicate,
lp-array × nat × lp-array × 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 | lp-array | partial function,
lp-array × nat × lp-array × nat × nat → lp-array |
| 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,
|
| disj | list-dup | predicate,
list × list |
| disj | nat-list-set | predicate,
nat-list × nat-list |
| dropn | list-prefixn | function,
nat × list → list |
| dropn | nat-list-set | function,
nat × nat-list → nat-list |
| dups | list-dup | predicate,
list |
| dups | nat-list-set | predicate,
nat-list |
| ebm-vol-inv | ebm-vol-inv | predicate,
avolume |
| 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 |
| err | error | variable,
error |
| err0 | error | variable,
error |
| err1 | error | variable,
error |
| error | error | sort,
|
| f | array-indices | variable,
elem → elem |
| 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 | lp-array | partial function,
lp-array × lprops × nat × nat → lp-array |
| fill | lp-array | function,
lp-array × lprops → lp-array |
| fill | avolume | partial function,
avolume × aleb × nat × nat → avolume |
| fill | avolume | function,
avolume × aleb → avolume |
| fillfirst | list-last | function,
nat × elem × list → list |
| fillfirst | nat-list-set | function,
nat × nat × nat-list → nat-list |
| firstn | list-del | partial function,
nat × list → list |
| firstn | nat-list-set | partial function,
nat × nat-list → nat-list |
| fn | array-indices | variable,
nat → nat |
| frome | list-del | function,
list × elem → list |
| frome | nat-list-set | function,
nat-list × nat → nat-list |
| idrange | buffer | partial predicate,
buffer × nat × nat |
| idrange | array-copy | partial predicate,
array × nat × nat |
| idrange | lp-array | partial predicate,
lp-array × nat × nat |
| idrange | avolume | partial predicate,
avolume × nat × nat |
| id○ | buffer | predicate,
buffer × buffer × nat |
| id○ | array-copy | predicate,
array × array × nat |
| id○ | lp-array | predicate,
lp-array × lp-array × nat |
| id○ | avolume | predicate,
avolume × avolume × nat |
| is-aligned | align | predicate,
nat × nat |
| isbuf | awbuf-asm | variable,
bool |
| isbuf | apersistence-io-asm | variable,
bool |
| isempty | eraseblock | predicate,
buffer × nat × nat |
| isempty | eraseblock | predicate,
buffer |
| lastn | list-del | partial function,
nat × list → list |
| lastn | nat-list-set | partial function,
nat × nat-list → nat-list |
| list | list-data | sort,
|
| log | apersistence-io-asm | variable,
nat-list |
| lp | lprops | variable,
lprops |
| lp-array | lp-array | sort,
|
| lp0 | lprops | variable,
lprops |
| lp1 | lp-array | variable,
lprops |
| lpf | lprops | variable,
lpropflags |
| lpf0 | lprops | variable,
lpropflags |
| lpropflags | lprops | sort,
|
| lprops | lprops | sort,
|
| lpt | lp-array | variable,
lp-array |
| lpt0 | lp-array | variable,
lp-array |
| lpt1 | lp-array | variable,
lp-array |
| lpt2 | lp-array | variable,
lp-array |
| lptfun | lp-array | variable,
lprops → lprops |
| m | nat-basic | variable,
nat |
| m0 | array-copy | variable,
nat |
| m0 | lprops | variable,
nat |
| m0 | bufleb | variable,
nat |
| m1 | wbuf | variable,
nat |
| m1 | lprops | variable,
nat |
| m2 | wbuf | variable,
nat |
| m2 | lprops | variable,
nat |
| m3 | lprops | variable,
nat |
| m4 | lprops | variable,
nat |
| mapped | aleb | function,
buffer → aleb |
| max | min-max | function,
nat × nat → nat |
| min | min-max | function,
nat × nat → nat |
| 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 |
| mklist | list-last | function,
elem × nat → list |
| mklist | nat-list-set | function,
nat × nat → nat-list |
| mklp | lprops | function,
nat × nat × lpropflags × nat → lprops |
| mklparray | lp-array | function,
nat → lp-array |
| mkwbuf | wbuf | function,
buffer × nat × nat → wbuf |
| 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 |
| n2 | nat-list-set | variable,
nat |
| n3 | nat-set | variable,
nat |
| n3 | nat-list-set | variable,
nat |
| n4 | nat-set | variable,
nat |
| n4 | nat-list-set | variable,
nat |
| n5 | nat-list-set | variable,
nat |
| nat | nat-basic | sort,
|
| nat-list | nat-list-set | sort,
|
| nat-set | nat-set | sort,
|
| nat-set | nat-list-set | sort,
|
| nobuffer | bufleb | constant,
bufleb |
| ns | nat-set | variable,
nat-set |
| ns | nat-list-set | variable,
nat-set |
| ns0 | nat-set | variable,
nat-set |
| ns0 | nat-list-set | variable,
nat-set |
| ns1 | nat-set | variable,
nat-set |
| ns1 | nat-list-set | variable,
nat-set |
| ns2 | nat-set | variable,
nat-set |
| ns2 | nat-list-set | variable,
nat-set |
| nx | nat-list-set | variable,
nat-list |
| nx0 | nat-list-set | variable,
nat-list |
| nx1 | nat-list-set | variable,
nat-list |
| ny | nat-list-set | variable,
nat-list |
| nz | nat-list-set | variable,
nat-list |
| plog | apersistence-io-asm | variable,
nat-list |
| pos | list-del | function,
elem × list → nat |
| pos | nat-list-set | function,
nat × nat-list → nat |
| prefixn | list-prefixn | function,
nat × list → list |
| prefixn | nat-list-set | function,
nat × nat-list → nat-list |
| 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 |
| restn | list-del | partial function,
nat × list → list |
| restn | nat-list-set | partial function,
nat × nat-list → nat-list |
| 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 | list-last | function,
list → list |
| rev | nat-list-set | function,
nat-list → nat-list |
| rev | lp-array | partial function,
lp-array × nat → lp-array |
| rev | lp-array | function,
lp-array → lp-array |
| rev | avolume | partial function,
avolume × nat → avolume |
| rev | avolume | function,
avolume → avolume |
| rmdup | list-dup | function,
list → list |
| rmdup | nat-list-set | function,
nat-list → nat-list |
| rofs | wbuf-base | variable,
bool |
| s | set-basic | variable,
set |
| s0 | set-basic | variable,
set |
| s1 | set-basic | variable,
set |
| s2 | set-basic | variable,
set |
| set | set-basic | sort,
|
| slice | list-prefixn | function,
nat × nat × list → list |
| slice | nat-list-set | function,
nat × nat × nat-list → nat-list |
| 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 |
| subarray | buffer | partial function,
buffer × nat × nat → buffer |
| subarray | array-copy | partial function,
array × nat × nat → array |
| subarray | lp-array | partial function,
lp-array × nat × nat → lp-array |
| subarray | avolume | partial function,
avolume × nat × nat → avolume |
| sublist | list-del | partial function,
nat × nat × list → list |
| sublist | nat-list-set | partial function,
nat × nat × nat-list → nat-list |
| synced | awbuf-inv | predicate,
avolume |
| unmapped | aleb | constant,
aleb |
| valid-indices | array-indices | predicate,
array × nat-list |
| valid-indices | lp-array | predicate,
lp-array × nat-list |
| wbuf | wbuf | variable,
wbuf |
| wbuf | wbuf | sort,
|
| wbuf-cons | wbuf-base | predicate,
wbuf × aleb × bool |
| wbuf-cons | wbuf-base | predicate,
bufleb × wbuf × avolume × bool |
| wbuf_add_log_leb# | wbuf-asm | procedure,
nat × nat × bool × address × nat × avolume × lp-array × nat-set
: bufleb × wbuf × nat-list
: error |
| wbuf_commit# | wbuf-asm | procedure,
lp-array × address × nat × avolume
: nat-set × address × nat × nat-list × lp-array × nat-set × bool
: error |
| wbuf_destroy_buf# | wbuf-asm | procedure,
bool : bufleb : error |
| wbuf_enter_readonly# | wbuf-asm | procedure,
: : bool |
| wbuf_format# | wbuf-asm | procedure,
nat × nat × lp-array × address × nat
: wbuf × nat × address × nat × nat-list × avolume × lp-array × nat-set ×
bufleb × bool
: error |
| wbuf_get_buf# | wbuf-asm | procedure,
bufleb : : bufleb |
| wbuf_get_leb_size# | wbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set : : nat |
| wbuf_get_page_size# | wbuf-asm | procedure,
nat : : nat |
| wbuf_get_volume_size# | wbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set : : nat |
| wbuf_is_readonly# | wbuf-asm | procedure,
bool : : bool |
| wbuf_move_buf# | wbuf-asm | procedure,
nat × nat × bool × avolume : bufleb × wbuf : error |
| wbuf_read_buf# | wbuf-asm | procedure,
nat × nat × nat × bufleb × wbuf × address × nat × nat-list × avolume ×
lp-array × nat-set
: buffer
: error |
| wbuf_recover# | wbuf-asm | procedure,
: address × nat × nat-set × nat-list × lp-array × wbuf × nat × address ×
nat × nat-list × avolume × lp-array × nat-set × bufleb × bool
: error |
| wbuf_remap# | wbuf-asm | procedure,
nat × bufleb × address × nat × nat-list × lp-array × nat-set
: avolume
: error |
| wbuf_requires_commit# | wbuf-asm | procedure,
address × nat × nat-list × avolume × lp-array × nat-set : : bool |
| wbuf_unmap# | wbuf-asm | procedure,
nat × bufleb × address × nat × nat-list × lp-array × nat-set : avolume |
| wbuf_write_buf# | wbuf-asm | procedure,
nat × buffer × bufleb × nat × address × nat × nat-list × lp-array ×
nat-set
: wbuf × bool × avolume
: error |
| x | list-data | variable,
list |
| x0 | list-data | variable,
list |
| x1 | list-data | variable,
list |
| y | list-data | variable,
list |
| z | list-data | variable,
list |
| zero | buffer | constant,
data |
| zero | array-splice | constant,
elem |
| zero | avolume | constant,
aleb |
| } | set-union | function,
elem → set |
| } | nat-set | function,
nat → nat-set |
| } | nat-list-set | function,
nat → nat-set |
| φ | array-indices | variable,
elem → bool |
| φ | lp-array | variable,
lprops → bool |
| φn | array-indices | variable,
nat → bool |
| ↓ | awbuf-inv | predicate,
aleb × aleb |
| ↓ | awbuf-inv | predicate,
avolume × avolume |
| ∅ | set-basic | constant,
set |
| ∅ | nat-set | constant,
nat-set |
| ∅ | nat-list-set | constant,
nat-set |
| ∈ | buffer | predicate,
data × buffer |
| ∈ | array-copy | predicate,
elem × array |
| ∈ | set-basic | predicate,
elem × set |
| ∈ | nat-set | predicate,
nat × nat-set |
| ∈ | list | predicate,
elem × list |
| ∈ | nat-list-set | predicate,
nat × nat-set |
| ∈ | nat-list-set | predicate,
nat × nat-list |
| ∈ | lp-array | predicate,
lprops × lp-array |
| ∈ | avolume | predicate,
aleb × avolume |
| ∩ | set-union | function,
set × set → set |
| ∩ | nat-set | function,
nat-set × nat-set → nat-set |
| ∩ | nat-list-set | function,
nat-set × nat-set → nat-set |
| ∪ | set-union | function,
set × set → set |
| ∪ | nat-set | function,
nat-set × nat-set → nat-set |
| ∪ | nat-list-set | function,
nat-set × nat-set → nat-set |
| ≤ | nat | predicate,
nat × nat |
| ≥ | nat | predicate,
nat × nat |
| ⊆ | set-basic | predicate,
set × set |
| ⊆ | nat-set | predicate,
nat-set × nat-set |
| ⊆ | ebm-vol-inv | predicate,
avolume × avolume |
| ⊆ | nat-list-set | predicate,
nat-set × nat-set |
| ⊑ | list-last | predicate,
list × list |
| ⊑ | nat-list-set | predicate,
nat-list × nat-list |
| ⊒ | list-last | predicate,
list × list |
| ⊒ | nat-list-set | predicate,
nat-list × nat-list |
| ⌋ | error-class | predicate,
error |