| Symbol | Specification | Kind | Type |
|---|---|---|---|
| # . | bag-union | f | bag → nat |
| # . | suffix-array-base | f | suffixarray → nat |
| . + . | suffix-array-base | f | suffixarray × suffixarray → suffixarray |
| . + . | nat-basic2 | f | nat × nat → nat |
| . ++ . | suffix-array-base | f | bag × nat → bag |
| . +1 | nat-basic1 | f | nat → nat |
| . - . | nat | f | nat × nat → nat |
| . -- . | suffix-array-base | f | bag × nat → bag |
| . -1 | nat-basic1 | f | nat → nat |
| . .elems | suffix-array-base | f | suffixarray → bag |
| . < . | nat-basic1 | p | nat × nat |
| . > . | nat | p | nat × nat |
| . [ . ] | suffix-array-base | f | suffixarray × nat → nat |
| . [ . ] | suffix-array-base | f | suffixarray × nat × nat → suffixarray |
| . \ . | bag-union | f | bag × bag → bag |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ∈ . | suffix-array-base | p | nat × suffixarray |
| . ∈ . | suffix-array-base | p | nat × bag |
| . ∪ . | bag-union | f | bag × bag → bag |
| . ⊆ . | bag-union | p | bag × bag |
| . elems . | suffix-array-base | f | suffixarray × nat → bag |
| { . } | suffix-array-base | f | nat → bag |
| ⊑ | suffix-array-base | v | nat × nat → bool |
| ∅ | bag-basic | c | bag |
| bag | bag-basic | s | |
| bag | bag-basic | v | bag |
| bag0 | bag-basic | v | bag |
| bag1 | bag-basic | v | bag |
| bag2 | bag-basic | v | bag |
| cmp | suffix-array-base | p | suffixarray × nat × nat × nat |
| cmp | suffix-array-base | p | suffixarray × nat × suffixarray × nat × nat |
| copy | suffix-array-base | f | suffixarray × nat × suffixarray × nat × nat → suffixarray |
| count | suffix-array-base | f | nat × bag → nat |
| empty | suffix-array-base | c | nat |
| fill | suffix-array-base | f | suffixarray × nat × nat × nat → suffixarray |
| fill | suffix-array-base | f | suffixarray × nat → suffixarray |
| id○ | suffix-array-base | p | suffixarray × suffixarray × nat |
| idrange | suffix-array-base | p | suffixarray × nat × nat |
| inv-inner | suffix-array-base | p | suffixarray × suffixarray × nat × nat × (nat × nat → bool) |
| inv-outer | suffix-array-base | p | suffixarray × suffixarray × nat × (nat × nat → bool) |
| k | suffix-array-base | v | nat |
| k0 | suffix-array-base | v | nat |
| k1 | suffix-array-base | v | nat |
| m | nat-basic2 | v | nat |
| m0 | array-copy | v | nat |
| max | min-max | f | nat × nat → nat |
| min | min-max | f | nat × nat → nat |
| mkemparray | suffix-array-base | f | nat → suffixarray |
| mksuffixarray | suffix-array-base | f | nat → suffixarray |
| mkzarray | suffix-array-base | f | nat → suffixarray |
| n | nat-basic1 | v | nat |
| n0 | nat-basic1 | v | nat |
| n1 | nat-basic1 | v | nat |
| nat | nat-basic1 | s | |
| pos | suffix-array-base | f | suffixarray × nat → nat |
| R | suffix-array-base | v | nat × nat → bool |
| range= | suffix-array-base | p | suffixarray × nat × suffixarray × nat × nat |
| reflexive | suffix-array-base | p | (nat × nat → bool) |
| resize | suffix-array-base | f | suffixarray × nat → suffixarray |
| sar | suffix-array-base | v | suffixarray |
| sar0 | suffix-array-base | v | suffixarray |
| sar1 | suffix-array-base | v | suffixarray |
| sar2 | suffix-array-base | v | suffixarray |
| sort# | suffix-array-base | pr | nat × nat → bool : suffixarray |
| sorted | suffix-array-base | p | suffixarray × nat × nat × (nat × nat → bool) |
| sorted | suffix-array-base | p | suffixarray × (nat × nat → bool) |
| splice | suffix-array-base | f | suffixarray × nat × suffixarray × nat × nat → suffixarray |
| subarray | suffix-array-base | f | suffixarray × nat × nat → suffixarray |
| suffixarray | suffix-array-base | s | |
| total | suffix-array-base | p | (nat × nat → bool) |
| transitive | suffix-array-base | p | (nat × nat → bool) |
| zero | suffix-array-base | c | nat |