| Symbol | Specification | Kind | Type |
|---|---|---|---|
| # . | bitlista | f | bitlist → nat |
| # . | valuetypes | f | valuetypes → nat |
| # . | bytelist | f | bytelist → nat |
| # . | references | f | referenceset → nat |
| # . | string-less | f | string → nat |
| # . | references | f | references → nat |
| # . | classnames | f | classnames → nat |
| # . | storekeys | f | storekeys → nat |
| # . | classnames | f | classnameset → nat |
| #oc | valuetypes | f | valuetype × valuetypes → nat |
| #oc | references | f | reference × references → nat |
| #oc | storekeys | f | storekey × storekeys → nat |
| #oc | bitlista | f | bool × bitlist → nat |
| #oc | classnames | f | classname × classnames → nat |
| #oc | bytelist | f | byte × bytelist → nat |
| . % . | int-div | f | int × int → int |
| . % . | nat-div | f | nat × nat → nat |
| . ' | string-append | f | char → string |
| . ' | valuetypes | f | valuetype → valuetypes |
| . ' | references | f | reference → references |
| . ' | bitlista | f | bool → bitlist |
| . ' | storekeys | f | storekey → storekeys |
| . ' | bytelist | f | byte → bytelist |
| . ' | storekey | f | int → storekey |
| . ' | classnames | f | classname → classnames |
| . ' | storekey | f | fieldspec → storekey |
| . * . | int-mult | f | int × int → int |
| . * . | nat-mult | f | nat × nat → nat |
| . + . | string-data | f | char × string → string |
| . + . | string-append | f | string × string → string |
| . + . | int-basic2 | f | int × int → int |
| . + . | valuetypes | f | valuetype × valuetype → valuetypes |
| . + . | nat-basic2 | f | nat × nat → nat |
| . + . | valuetypes | f | valuetypes × valuetype → valuetypes |
| . + . | bitlista | f | bool × bitlist → bitlist |
| . + . | valuetypes | f | valuetypes × valuetypes → valuetypes |
| . + . | bitlista | f | bitlist × bitlist → bitlist |
| . + . | valuetypes | f | valuetype × valuetypes → valuetypes |
| . + . | bitlista | f | bitlist × bool → bitlist |
| . + . | references | f | reference × reference → references |
| . + . | bitlista | f | bool × bool → bitlist |
| . + . | references | f | references × reference → references |
| . + . | bytelist | f | byte × bytelist → bytelist |
| . + . | references | f | references × references → references |
| . + . | bytelist | f | bytelist × bytelist → bytelist |
| . + . | references | f | reference × references → references |
| . + . | bytelist | f | bytelist × byte → bytelist |
| . + . | storekeys | f | storekey × storekey → storekeys |
| . + . | bytelist | f | byte × byte → bytelist |
| . + . | storekeys | f | storekeys × storekey → storekeys |
| . + . | classnames | f | classname × classnames → classnames |
| . + . | storekeys | f | storekeys × storekeys → storekeys |
| . + . | classnames | f | classnames × classnames → classnames |
| . + . | storekeys | f | storekey × storekeys → storekeys |
| . + . | classnames | f | classnames × classname → classnames |
| . + . | classnames | f | classname × classname → classnames |
| . ++ . | valuetypes | f | valuetypes × valuetype → valuetypes |
| . ++ . | bitlista | f | bitlist × bool → bitlist |
| . ++ . | javavalue | f | javavalue × javavalue → javavalue |
| . ++ . | bytelist | f | bytelist × byte → bytelist |
| . ++ . | references | f | referenceset × reference → referenceset |
| . ++ . | classnames | f | classnames × classname → classnames |
| . ++ . | references | f | references × reference → references |
| . ++ . | classnames | f | classnameset × classname → classnameset |
| . ++ . | storekeys | f | storekeys × storekey → storekeys |
| . +1 | int-basic1 | f | int → int |
| . +1 | bitopsaux | f | bitlist → bitlist |
| . +1 | nat-basic1 | f | nat → nat |
| . - . | int-abs | f | int × int → int |
| . - . | nat | f | nat × nat → nat |
| . -- . | references | f | referenceset × reference → referenceset |
| . -- . | refkey | f | reference × storekey → refkey |
| . -- . | classnames | f | classnameset × classname → classnameset |
| . -1 | int-basic1 | f | int → int |
| . -1 | nat-basic1 | f | nat → nat |
| . -1l . | valuetypes | f | valuetypes × nat → valuetypes |
| . -1l . | valuetypes | f | valuetypes × valuetype → valuetypes |
| . -1l . | bitlista | f | bitlist × bool → bitlist |
| . -1l . | references | f | references × nat → references |
| . -1l . | bitlista | f | bitlist × nat → bitlist |
| . -1l . | references | f | references × reference → references |
| . -1l . | bytelist | f | bytelist × byte → bytelist |
| . -1l . | storekeys | f | storekeys × nat → storekeys |
| . -1l . | bytelist | f | bytelist × nat → bytelist |
| . -1l . | storekeys | f | storekeys × storekey → storekeys |
| . -1l . | classnames | f | classnames × classname → classnames |
| . -1l . | classnames | f | classnames × nat → classnames |
| . -l . | bitlista | f | bitlist × bool → bitlist |
| . -l . | valuetypes | f | valuetypes × valuetype → valuetypes |
| . -l . | bytelist | f | bytelist × byte → bytelist |
| . -l . | references | f | references × reference → references |
| . -l . | classnames | f | classnames × classname → classnames |
| . -l . | storekeys | f | storekeys × storekey → storekeys |
| . .boolval | javavalue | p | javavalue |
| . .butlast | bitlista | f | bitlist → bitlist |
| . .butlast | valuetypes | f | valuetypes → valuetypes |
| . .butlast | bytelist | f | bytelist → bytelist |
| . .butlast | classnames | f | classnames → classnames |
| . .butlast | storekeys | f | storekeys → storekeys |
| . .butlast | references | f | references → references |
| . .butmax | references | f | referenceset → referenceset |
| . .butmax | classnames | f | classnameset → classnameset |
| . .butmin | classnames | f | classnameset → classnameset |
| . .butmin | references | f | referenceset → referenceset |
| . .byteval | javavalue | f | javavalue → byte |
| . .char1 | string-data | f | string → char |
| . .charval | javavalue | f | javavalue → javachar |
| . .class | classname | f | string → classname |
| . .class | fieldspec | f | fieldspec → classname |
| . .class | classname | f | classname → string |
| . .class | javatype | f | javatype → classname |
| . .doubleval | javavalue | f | javavalue → double |
| . .field | fieldname | f | string → fieldname |
| . .field | fieldspec | f | fieldspec → fieldname |
| . .field | fieldname | f | fieldname → string |
| . .first | bitlista | p | bitlist |
| . .first | bytelist | f | bytelist → byte |
| . .first | valuetypes | f | valuetypes → valuetype |
| . .first | classnames | f | classnames → classname |
| . .first | storekeys | f | storekeys → storekey |
| . .first | references | f | references → reference |
| . .firstval | javavalue | f | javavalue → javavalue |
| . .floatval | javavalue | f | javavalue → float |
| . .fs | storekey | f | storekey → fieldspec |
| . .index | storekey | f | storekey → int |
| . .int | javachar | f | javachar → int |
| . .int | float | f | float → int |
| . .int | float | f | double → int |
| . .intval | javavalue | f | javavalue → int |
| . .istate | javavalue | f | javavalue → initstate |
| . .jtclass | typefuns | f | javatype → classname |
| . .jtdims | typefuns | f | javatype → int |
| . .jtelemtype | typefuns | f | javatype → javatype |
| . .key | refkey | f | refkey → storekey |
| . .label | label | f | string → label |
| . .label | javavalue | f | javavalue → label |
| . .label | label | f | label → string |
| . .last | bitlista | p | bitlist |
| . .last | valuetypes | f | valuetypes → valuetype |
| . .last | bytelist | f | bytelist → byte |
| . .last | classnames | f | classnames → classname |
| . .last | references | f | references → reference |
| . .last | storekeys | f | storekeys → storekey |
| . .longval | javavalue | f | javavalue → long |
| . .max | references | f | referenceset → reference |
| . .max | classnames | f | classnameset → classname |
| . .min | classnames | f | classnameset → classname |
| . .min | references | f | referenceset → reference |
| . .ref | refkey | f | refkey → reference |
| . .refval | javavalue | f | javavalue → reference |
| . .rest | bitlista | f | bitlist → bitlist |
| . .rest | valuetypes | f | valuetypes → valuetypes |
| . .rest | bytelist | f | bytelist → bytelist |
| . .rest | classnames | f | classnames → classnames |
| . .rest | references | f | references → references |
| . .rest | storekeys | f | storekeys → storekeys |
| . .restval | javavalue | f | javavalue → javavalue |
| . .rstring | string-data | f | string → string |
| . .shortval | javavalue | f | javavalue → short |
| . .stringval | javavalue | f | javavalue → string |
| . .type | value+type | f | valuetype → javatype |
| . .type | javatype | f | javatype → javatype |
| . .type | fieldspec | f | fieldspec → javatype |
| . .type | javavalue | f | javavalue → javatype |
| . .val | value+type | f | valuetype → javavalue |
| . .val | javavalue | f | javavalue → javavalue |
| . / . | int-div | f | int × int → int |
| . / . | nat-div | f | nat × nat → nat |
| . < . | valuetypes | p | valuetypes × valuetypes |
| . < . | references | p | referenceset × reference |
| . < . | references | p | reference × referenceset |
| . < . | references | p | references × references |
| . < . | storekeys | p | storekeys × storekeys |
| . < . | int-basic1 | p | int × int |
| . < . | specialkeys | p | refkey × refkey |
| . < . | nat-basic1 | p | nat × nat |
| . < . | reference | p | reference × reference |
| . < . | bitlista | p | bitlist × bitlist |
| . < . | classnames | p | classnameset × classname |
| . < . | bytelist | p | bytelist × bytelist |
| . < . | classnames | p | classname × classnameset |
| . < . | string-less | p | string × string |
| . < . | classnames | p | classnames × classnames |
| . < . | string-less | p | char × char |
| . << . | intops | f | int × int → int |
| . <_1 . | classnamefuns | p | classname × classname |
| . > . | nat | p | nat × nat |
| . > . | int-abs | p | int × int |
| . >> . | intops | f | int × int → int |
| . [ . ] | bitlista | f | bitlist × nat × bool → bitlist |
| . [ . ] | bitlista | p | bitlist × nat |
| . [ . ] | valuetypes | f | valuetypes × nat × valuetype → valuetypes |
| . [ . ] | bytelist | f | bytelist × nat → byte |
| . [ . ] | valuetypes | f | valuetypes × nat → valuetype |
| . [ . ] | bytelist | f | bytelist × nat × byte → bytelist |
| . [ . ] | valuefuns | f | javavalue × reference × reference → javavalue |
| . [ . ] | classnames | f | classnames × nat → classname |
| . [ . ] | references | f | references × nat × reference → references |
| . [ . ] | classnames | f | classnames × nat × classname → classnames |
| . [ . ] | references | f | references × nat → reference |
| . [ . ] | storekeys | f | storekeys × nat → storekey |
| . [ . ] | storekeys | f | storekeys × nat × storekey → storekeys |
| . \ . | bitlista | f | bitlist × bitlist → bitlist |
| . \ . | valuetypes | f | valuetypes × valuetypes → valuetypes |
| . \ . | bytelist | f | bytelist × bytelist → bytelist |
| . \ . | references | f | referenceset × referenceset → referenceset |
| . \ . | classnames | f | classnames × classnames → classnames |
| . \ . | references | f | references × references → references |
| . \ . | classnames | f | classnameset × classnameset → classnameset |
| . \ . | storekeys | f | storekeys × storekeys → storekeys |
| . ^ . | int-pot | f | int × int → int |
| . ^2 | int-square | f | int → int |
| . ≤ . | typefuns | p | javatype × javatype |
| . ≤ . | int-abs | p | int × int |
| . ≤ . | classnamefuns | p | classname × classname |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | int-abs | p | int × int |
| . ≥ . | nat | p | nat × nat |
| . ∈ . | valuetypes | p | valuetype × valuetypes |
| . ∈ . | valuefuns | p | reference × javavalue |
| . ∈ . | bitlista | p | bool × bitlist |
| . ∈ . | references | p | reference × referenceset |
| . ∈ . | references | p | reference × references |
| . ∈ . | storekeys | p | storekey × storekeys |
| . ∈ . | bytelist | p | byte × bytelist |
| . ∈ . | classnames | p | classname × classnameset |
| . ∈ . | classnames | p | classname × classnames |
| . ∈bint | byte | p | int |
| . ∈byte | byte | p | int |
| . ∈long | byte | p | int |
| . ∈short | byte | p | int |
| . ∪ . | bitlista | f | bitlist × bitlist → bitlist |
| . ∪ . | valuetypes | f | valuetypes × valuetypes → valuetypes |
| . ∪ . | bytelist | f | bytelist × bytelist → bytelist |
| . ∪ . | classnames | f | classnames × classnames → classnames |
| . ∪ . | references | f | referenceset × referenceset → referenceset |
| . ∪ . | classnames | f | classnameset × classnameset → classnameset |
| . ∪ . | references | f | references × references → references |
| . ∪ . | storekeys | f | storekeys × storekeys → storekeys |
| . ∩ . | references | f | referenceset × referenceset → referenceset |
| . ∩ . | classnames | f | classnameset × classnameset → classnameset |
| . ⊆ . | valuetypes | p | valuetypes × valuetypes |
| . ⊆ . | bitlista | p | bitlist × bitlist |
| . ⊆ . | references | p | referenceset × referenceset |
| . ⊆ . | bytelist | p | bytelist × bytelist |
| . ⊆ . | references | p | references × references |
| . ⊆ . | classnames | p | classnames × classnames |
| . ⊆ . | storekeys | p | storekeys × storekeys |
| . ⊆ . | classnames | p | classnameset × classnameset |
| . ⊆m . | valuetypes | p | valuetypes × valuetypes |
| . ⊆m . | references | p | references × references |
| . ⊆m . | bitlista | p | bitlist × bitlist |
| . ⊆m . | storekeys | p | storekeys × storekeys |
| . ⊆m . | bytelist | p | bytelist × bytelist |
| . ⊆m . | classnames | p | classnames × classnames |
| . × . | value+type | f | javavalue × javatype → valuetype |
| . ⊑ . | valuetypes | p | valuetypes × valuetypes |
| . ⊑ . | bitlista | p | bitlist × bitlist |
| . ⊑ . | references | p | references × references |
| . ⊑ . | bytelist | p | bytelist × bytelist |
| . ⊑ . | storekeys | p | storekeys × storekeys |
| . ⊑ . | classnames | p | classnames × classnames |
| . ⊒ . | valuetypes | p | valuetypes × valuetypes |
| . ⊒ . | references | p | references × references |
| . ⊒ . | bitlista | p | bitlist × bitlist |
| . ⊒ . | storekeys | p | storekeys × storekeys |
| . ⊒ . | bytelist | p | bytelist × bytelist |
| . ⊒ . | classnames | p | classnames × classnames |
| . i<< . | intops | f | int × int → int |
| . i>> . | intops | f | int × int → int |
| . i>>> . | intops | f | int × int → int |
| . l< . | classnamefuns | p | classname × classname |
| . l<< . | intops | f | int × int → int |
| . l>> . | intops | f | int × int → int |
| . l>>> . | intops | f | int × int → int |
| >>> | intops | f | nat × int × int → int |
| [] | bitlista | c | bitlist |
| [] | bytelist | c | bytelist |
| [] | valuetypes | c | valuetypes |
| [] | classnames | c | classnames |
| [] | references | c | references |
| [] | storekeys | c | storekeys |
| _endfinallymode | specialkeys | c | refkey |
| _initfield | specialkeys | c | fieldname |
| _length | specialkeys | c | storekey |
| _mode | specialkeys | c | refkey |
| _out | specialkeys | c | refkey |
| _type | specialkeys | c | storekey |
| _uninit | specialkeys | c | refkey |
| { . } | references | f | reference → referenceset |
| { . } | classnames | f | classname → classnameset |
| ~ . | int-abs | f | int → int |
| ∅ | classnames | c | classnameset |
| ∅ | references | c | referenceset |
| 0b | byte | c | byte |
| 0bi | byte | c | bint |
| 0d | float | c | double |
| 0f | float | c | float |
| 0l | byte | c | long |
| 0s | byte | c | short |
| abs | int-abs | f | int → int |
| abstract_type | javatype | c | javatype |
| b2bi | byte | f | byte → bint |
| b2i | byte | f | byte → int |
| b2s | byte | f | byte → short |
| band | intops | f | int × int → int |
| bcompl | intops | f | int → int |
| bi | byte | v | bint |
| bi2b | byte | f | bint → byte |
| bi2i | byte | f | bint → int |
| bi2s | byte | f | bint → short |
| bint | byte | s | |
| bitlist | bitlista | s | |
| bits | bitlista | v | bitlist |
| bits0 | bitlista | v | bitlist |
| bits1 | bitlista | v | bitlist |
| bits10 | bitlista | v | bitlist |
| bits2 | bitlista | v | bitlist |
| bits2bytes | bytes | f | bitlist → bytelist |
| bits2int | int2bits | f | bitlist → int |
| bits2uint | int2bits | f | bitlist → int |
| bits3 | bitlista | v | bitlist |
| bits4 | bitlista | v | bitlist |
| bits5 | bitlista | v | bitlist |
| bits6 | bitlista | v | bitlist |
| bits7 | bitlista | v | bitlist |
| bits8 | bitlista | v | bitlist |
| bits9 | bitlista | v | bitlist |
| bitsand | intops | f | bitlist × bitlist → bitlist |
| bitsinvert | bitopsaux | f | bitlist → bitlist |
| bitsor | intops | f | bitlist × bitlist → bitlist |
| bitsxor | intops | f | bitlist × bitlist → bitlist |
| bj | byte | v | bint |
| bool | bool | s | |
| boolean_type | javatype | c | javatype |
| boolval | javavalue | f | bool → javavalue |
| boolvar | bool | v | bool |
| boolvar0 | bool | v | bool |
| boolvar1 | bitlista | v | bool |
| boolvar2 | bitlista | v | bool |
| bor | intops | f | int × int → int |
| break | javavalue | f | label → javavalue |
| butlastn | bitlista | f | nat × bitlist → bitlist |
| butlastn | valuetypes | f | nat × valuetypes → valuetypes |
| butlastn | bytelist | f | nat × bytelist → bytelist |
| butlastn | references | f | nat × references → references |
| butlastn | classnames | f | nat × classnames → classnames |
| butlastn | storekeys | f | nat × storekeys → storekeys |
| bxor | intops | f | int × int → int |
| by | byte | v | byte |
| by0 | bytelist | v | byte |
| by1 | bytelist | v | byte |
| by2 | bytelist | v | byte |
| byi | byte | v | byte |
| byj | byte | v | byte |
| byte | byte | s | |
| byte_type | javatype | c | javatype |
| byte2bits | bytes | f | byte → bitlist |
| bytelist | bytelist | s | |
| bytes | bytelist | v | bytelist |
| bytes0 | bytelist | v | bytelist |
| bytes1 | bytelist | v | bytelist |
| bytes10 | bytelist | v | bytelist |
| bytes2 | bytelist | v | bytelist |
| bytes2bits | bytes | f | bytelist → bitlist |
| bytes2int | bytes | f | bytelist → int |
| bytes3 | bytelist | v | bytelist |
| bytes4 | bytelist | v | bytelist |
| bytes5 | bytelist | v | bytelist |
| bytes6 | bytelist | v | bytelist |
| bytes7 | bytelist | v | bytelist |
| bytes8 | bytelist | v | bytelist |
| bytes9 | bytelist | v | bytelist |
| byteval | javavalue | f | byte → javavalue |
| cast | intops | f | int × int → int |
| char | char | s | |
| char | char | v | char |
| char_type | javatype | c | javatype |
| char0 | char | v | char |
| char1 | char | v | char |
| char2 | char | v | char |
| char3 | string-less | v | char |
| charval | javavalue | f | javachar → javavalue |
| claset | classnames | v | classnameset |
| claset0 | classnames | v | classnameset |
| claset1 | classnames | v | classnameset |
| claset2 | classnames | v | classnameset |
| class | classname | v | classname |
| class+∃ | typefuns | p | string × classname |
| class∃ | typefuns | p | string × classname |
| class0 | classname | v | classname |
| class1 | classname | v | classname |
| class2 | classname | v | classname |
| class3 | classname | v | classname |
| classes | classnames | v | classnames |
| classes0 | classnames | v | classnames |
| classes1 | classnames | v | classnames |
| classes10 | classnames | v | classnames |
| classes2 | classnames | v | classnames |
| classes3 | classnames | v | classnames |
| classes4 | classnames | v | classnames |
| classes5 | classnames | v | classnames |
| classes6 | classnames | v | classnames |
| classes7 | classnames | v | classnames |
| classes8 | classnames | v | classnames |
| classes9 | classnames | v | classnames |
| classname | classname | s | |
| classnames | classnames | s | |
| classnameset | classnames | s | |
| coerce | valuefuns | f | javavalue × javatype → javavalue |
| continue | javavalue | f | label → javavalue |
| disj | valuetypes | p | valuetypes × valuetypes |
| disj | references | p | references × references |
| disj | storekeys | p | storekeys × storekeys |
| disj | bitlista | p | bitlist × bitlist |
| disj | classnames | p | classnames × classnames |
| disj | bytelist | p | bytelist × bytelist |
| done | initstate | c | initstate |
| double | float | s | |
| double_type | javatype | c | javatype |
| doubleval | javavalue | f | double → javavalue |
| doublevar | float | v | double |
| doublevar0 | javavalue | v | double |
| dups | valuetypes | p | valuetypes |
| dups | bitlista | p | bitlist |
| dups | references | p | references |
| dups | bytelist | p | bytelist |
| dups | storekeys | p | storekeys |
| dups | classnames | p | classnames |
| error | initstate | c | initstate |
| even | int-min | p | int |
| fieldname | fieldname | s | |
| fieldspec | fieldspec | s | |
| fieldvar | fieldname | v | fieldname |
| fieldvar0 | fieldname | v | fieldname |
| fieldvar1 | fieldname | v | fieldname |
| fieldvar2 | fieldname | v | fieldname |
| fieldvar3 | fieldname | v | fieldname |
| fillfirst | bitlista | f | nat × bool × bitlist → bitlist |
| fillfirst | valuetypes | f | nat × valuetype × valuetypes → valuetypes |
| fillfirst | references | f | nat × reference × references → references |
| fillfirst | bytelist | f | nat × byte × bytelist → bytelist |
| fillfirst | storekeys | f | nat × storekey × storekeys → storekeys |
| fillfirst | classnames | f | nat × classname × classnames → classnames |
| fillsgn | bitopsaux | f | nat × bitlist → bitlist |
| fillsgn | bytes | f | nat × bytelist → bytelist |
| filter | valuetypes | f | valuetypes × valuetypes → valuetypes |
| filter | references | f | references × references → references |
| filter | bitlista | f | bitlist × bitlist → bitlist |
| filter | storekeys | f | storekeys × storekeys → storekeys |
| filter | bytelist | f | bytelist × bytelist → bytelist |
| filter | classnames | f | classnames × classnames → classnames |
| firstn | bitlista | f | nat × bitlist → bitlist |
| firstn | valuetypes | f | nat × valuetypes → valuetypes |
| firstn | references | f | nat × references → references |
| firstn | bytelist | f | nat × bytelist → bytelist |
| firstn | storekeys | f | nat × storekeys → storekeys |
| firstn | classnames | f | nat × classnames → classnames |
| fix | bitopsaux | f | nat × bitlist → bitlist |
| fix | bytes | f | nat × bytelist → bytelist |
| flatten | valuefuns | f | javavalue → javavalue |
| float | float | s | |
| float_type | javatype | c | javatype |
| floatval | javavalue | f | float → javavalue |
| floatvar | float | v | float |
| floatvar0 | javavalue | v | float |
| frome | bitlista | f | bitlist × bool → bitlist |
| frome | bytelist | f | bytelist × byte → bytelist |
| frome | classnames | f | classnames × classname → classnames |
| frome | valuetypes | f | valuetypes × valuetype → valuetypes |
| frome | storekeys | f | storekeys × storekey → storekeys |
| frome | references | f | references × reference → references |
| fs | fieldspec | v | fieldspec |
| fs0 | fieldspec | v | fieldspec |
| fs1 | fieldspec | v | fieldspec |
| get | valuefuns | f | nat × javavalue → javavalue |
| getrange | valuefuns | f | nat × nat × javavalue → javavalue |
| has_classtype | typefuns | p | javatype |
| i | int-basic1 | v | int |
| i→n | intnat | f | int → nat |
| i0 | int-basic1 | v | int |
| i2b | byte | f | int → byte |
| i2bi | byte | f | int → bint |
| i2l | byte | f | int → long |
| i2s | byte | f | int → short |
| incdec | valuefuns | f | javavalue × int → javavalue |
| initial_value | valuefuns | f | javatype → javavalue |
| initstate | initstate | s | |
| initval | javavalue | f | initstate → javavalue |
| ins≤ | classnames | f | classname × classnames → classnames |
| ins≤ | references | f | reference × references → references |
| int | int-basic1 | s | |
| int_type | javatype | c | javatype |
| int2bits | int2bits | f | int → bitlist |
| int2bytes | bytes | f | int → bytelist |
| interface∃ | typefuns | p | string × classname |
| intval | javavalue | f | int → javavalue |
| is_abstract | typefuns | p | classname |
| is_arraytype | javatype | p | javatype |
| is_boolvalue | javavalue | p | javavalue |
| is_break_mode | javavalue | p | javavalue |
| is_bytevalue | javavalue | p | javavalue |
| is_charvalue | javavalue | p | javavalue |
| is_classtype | javatype | p | javatype |
| is_continue_mode | javavalue | p | javavalue |
| is_doublevalue | javavalue | p | javavalue |
| is_floatvalue | javavalue | p | javavalue |
| is_fskey | storekey | p | storekey |
| is_indexkey | storekey | p | storekey |
| is_initvalue | javavalue | p | javavalue |
| is_integervalue | javavalue | p | javavalue |
| is_longvalue | javavalue | p | javavalue |
| is_normal_mode | valuefuns | p | javavalue |
| is_novalue | javavalue | p | javavalue |
| is_predefined_class | predefined | p | classname |
| is_primtype | typefuns | p | javatype |
| is_referencevalue | javavalue | p | javavalue |
| is_reftype | typefuns | p | javatype |
| is_return_mode | javavalue | p | javavalue |
| is_shortvalue | javavalue | p | javavalue |
| is_stringvalue | javavalue | p | javavalue |
| is_subclass | typefuns | p | classname × classnames × classname |
| is_subtype | typefuns | p | string × javatype × javatype |
| is_subtype | typefuns | p | javatype × classnames × javatype |
| is_subtype | typefuns | p | javatype × javatype × classnameset |
| is_throw_mode | javavalue | p | javavalue |
| is_typevalue | javavalue | p | javavalue |
| is_valuelist | javavalue | p | javavalue |
| is_void_type | javatype | p | javatype |
| istate | initstate | v | initstate |
| istate0 | javavalue | v | initstate |
| j | int-basic1 | v | int |
| j0 | int-basic1 | v | int |
| javachar | javachar | s | |
| javatype | javatype | s | |
| javavalue | javavalue | s | |
| jchar | javachar | v | javachar |
| jchar0 | javachar | v | javachar |
| jchar1 | javachar | v | javachar |
| jchar2 | javachar | v | javachar |
| jvmref | reference | c | reference |
| l2i | byte | f | long → int |
| label | label | s | |
| lastn | bitlista | f | nat × bitlist → bitlist |
| lastn | bytelist | f | nat × bytelist → bytelist |
| lastn | classnames | f | nat × classnames → classnames |
| lastn | storekeys | f | nat × storekeys → storekeys |
| lastn | references | f | nat × references → references |
| lastn | valuetypes | f | nat × valuetypes → valuetypes |
| lbl | label | v | label |
| lbl0 | label | v | label |
| lbl1 | label | v | label |
| lbl2 | label | v | label |
| list2set | classnames | f | classnames → classnameset |
| list2set | references | f | references → referenceset |
| lo | byte | v | long |
| lo0 | javavalue | v | long |
| loi | byte | v | long |
| loj | byte | v | long |
| long | byte | s | |
| long_type | javatype | c | javatype |
| longval | javavalue | f | long → javavalue |
| m | nat-basic2 | v | nat |
| max | int-min | f | int × int → int |
| merge | references | f | references × references → references |
| merge | classnames | f | classnames × classnames → classnames |
| min | int-min | f | int × int → int |
| mkarraytype | javatype | f | javatype → javatype |
| mkchar | javachar | f | string → javachar |
| mkchar | javachar | f | int → javachar |
| mkclasstype | javatype | f | classname → javatype |
| mkdouble | float | f | string → double |
| mkfloat | float | f | string → float |
| mkfs | fieldspec | f | classname × javatype × fieldname → fieldspec |
| mklist | valuetypes | f | valuetype × nat → valuetypes |
| mklist | bitlista | f | bool × nat → bitlist |
| mklist | references | f | reference × nat → references |
| mklist | bytelist | f | byte × nat → bytelist |
| mklist | storekeys | f | storekey × nat → storekeys |
| mklist | classnames | f | classname × nat → classnames |
| mktype_from_dims | typefuns | f | javatype × int → javatype |
| n | nat-basic1 | v | nat |
| n→i | intnat | f | nat → int |
| n0 | nat-basic1 | v | nat |
| n1 | nat-basic1 | v | nat |
| nat | nat-basic1 | s | |
| next | reference | f | reference → reference |
| noval | javavalue | c | javavalue |
| odd | int-min | p | int |
| okprimtype | valuefuns | p | javavalue × javatype |
| okval | valuefuns | p | javavalue × javatype |
| ordered< | references | p | references |
| ordered< | classnames | p | classnames |
| ordered≤ | classnames | p | classnames |
| ordered≤ | references | p | references |
| perm | valuetypes | p | valuetypes × valuetypes |
| perm | references | p | references × references |
| perm | bitlista | p | bitlist × bitlist |
| perm | storekeys | p | storekeys × storekeys |
| perm | bytelist | p | bytelist × bytelist |
| perm | classnames | p | classnames × classnames |
| pos | bitlista | f | bool × bitlist → nat |
| pos | valuetypes | f | valuetype × valuetypes → nat |
| pos | bytelist | f | byte × bytelist → nat |
| pos | references | f | reference × references → nat |
| pos | string-less | f | char × string → nat |
| pos | storekeys | f | storekey × storekeys → nat |
| pos | classnames | f | classname × classnames → nat |
| predef_superClass | predefined | f | classname → classname |
| predef_supers | predefined | f | classname → classnames |
| predefined_classes | predefined | c | classnames |
| r | reference | v | reference |
| r0 | reference | v | reference |
| r1 | reference | v | reference |
| r2 | reference | v | reference |
| reference | reference | s | |
| references | references | s | |
| referenceset | references | s | |
| refkey | refkey | s | |
| refp | valuefuns | p | javavalue |
| refs | references | v | references |
| refs0 | references | v | references |
| refs1 | references | v | references |
| refs10 | references | v | references |
| refs2 | references | v | references |
| refs3 | references | v | references |
| refs4 | references | v | references |
| refs5 | references | v | references |
| refs6 | references | v | references |
| refs7 | references | v | references |
| refs8 | references | v | references |
| refs9 | references | v | references |
| refval | javavalue | f | reference → javavalue |
| restn | bitlista | f | nat × bitlist → bitlist |
| restn | valuetypes | f | nat × valuetypes → valuetypes |
| restn | bytelist | f | nat × bytelist → bytelist |
| restn | classnames | f | nat × classnames → classnames |
| restn | references | f | nat × references → references |
| restn | storekeys | f | nat × storekeys → storekeys |
| return | javavalue | f | javavalue × javatype → javavalue |
| rev | bitlista | f | bitlist → bitlist |
| rev | bytelist | f | bytelist → bytelist |
| rev | classnames | f | classnames → classnames |
| rev | storekeys | f | storekeys → storekeys |
| rev | references | f | references → references |
| rev | valuetypes | f | valuetypes → valuetypes |
| rk | refkey | v | refkey |
| rk0 | refkey | v | refkey |
| rk1 | refkey | v | refkey |
| rk2 | refkey | v | refkey |
| rmdup | bitlista | f | bitlist → bitlist |
| rmdup | bytelist | f | bytelist → bytelist |
| rmdup | valuetypes | f | valuetypes → valuetypes |
| rmdup | classnames | f | classnames → classnames |
| rmdup | references | f | references → references |
| rmdup | storekeys | f | storekeys → storekeys |
| rset | references | v | referenceset |
| rset0 | references | v | referenceset |
| rset1 | references | v | referenceset |
| rset2 | references | v | referenceset |
| s→r | valuefuns | f | string → reference |
| s2b | byte | f | short → byte |
| s2bi | byte | f | short → bint |
| s2i | byte | f | short → int |
| set2list | references | f | referenceset → references |
| set2list | classnames | f | classnameset → classnames |
| sgn | int-min | f | int → int |
| sgn | bitopsaux | f | bitlist → bitlist |
| shiftright | valuefuns | f | javavalue → javavalue |
| sho | byte | v | short |
| sho0 | javavalue | v | short |
| shoi | byte | v | short |
| shoj | byte | v | short |
| short | byte | s | |
| short_type | javatype | c | javatype |
| shortOverflow | byte | p | int |
| shortval | javavalue | f | short → javavalue |
| sk | storekey | v | storekey |
| sk0 | storekey | v | storekey |
| sk1 | storekey | v | storekey |
| sk2 | storekeys | v | storekey |
| sks | storekeys | v | storekeys |
| sks0 | storekeys | v | storekeys |
| sks1 | storekeys | v | storekeys |
| sks10 | storekeys | v | storekeys |
| sks2 | storekeys | v | storekeys |
| sks3 | storekeys | v | storekeys |
| sks4 | storekeys | v | storekeys |
| sks5 | storekeys | v | storekeys |
| sks6 | storekeys | v | storekeys |
| sks7 | storekeys | v | storekeys |
| sks8 | storekeys | v | storekeys |
| sks9 | storekeys | v | storekeys |
| sortedchars | string-less | c | string |
| sqrt | int-square | f | int → int |
| storekey | storekey | s | |
| storekeys | storekeys | s | |
| str | string-data | v | string |
| str0 | string-data | v | string |
| str1 | string-data | v | string |
| str2 | string-data | v | string |
| str3 | string-data | v | string |
| string | string-data | s | |
| stringval | javavalue | f | string → javavalue |
| stringvar | string-append | v | string |
| stringvar0 | string-append | v | string |
| sublist | bitlista | f | nat × nat × bitlist → bitlist |
| sublist | bytelist | f | nat × nat × bytelist → bytelist |
| sublist | valuetypes | f | nat × nat × valuetypes → valuetypes |
| sublist | classnames | f | nat × nat × classnames → classnames |
| sublist | references | f | nat × nat × references → references |
| sublist | storekeys | f | nat × nat × storekeys → storekeys |
| tdname+∃ | typefuns | p | string × classname |
| tdname∃ | typefuns | p | string × classname |
| this | reference | v | reference |
| throw | javavalue | f | reference × javatype → javavalue |
| ty | javatype | v | javatype |
| ty0 | javatype | v | javatype |
| ty1 | javatype | v | javatype |
| ty2 | javatype | v | javatype |
| type∃ | typefuns | p | string × javatype |
| type4value | valuefuns | f | javavalue → javatype |
| typeval | javavalue | f | javatype → javavalue |
| ub2i | byte | f | byte → int |
| uint2bits | int2bits | f | int → bitlist |
| undone | initstate | c | initstate |
| us2i | byte | f | short → int |
| val | javavalue | v | javavalue |
| val0 | javavalue | v | javavalue |
| val1 | javavalue | v | javavalue |
| val2 | javavalue | v | javavalue |
| val2int | valuefuns | f | javavalue → int |
| valuetype | value+type | s | |
| valuetypes | valuetypes | s | |
| void_type | javatype | c | javatype |
| vt | value+type | v | valuetype |
| vt0 | value+type | v | valuetype |
| vt1 | value+type | v | valuetype |
| vt2 | value+type | v | valuetype |
| vts | valuetypes | v | valuetypes |
| vts0 | valuetypes | v | valuetypes |
| vts1 | valuetypes | v | valuetypes |
| vts10 | valuetypes | v | valuetypes |
| vts2 | valuetypes | v | valuetypes |
| vts3 | valuetypes | v | valuetypes |
| vts4 | valuetypes | v | valuetypes |
| vts5 | valuetypes | v | valuetypes |
| vts6 | valuetypes | v | valuetypes |
| vts7 | valuetypes | v | valuetypes |
| vts8 | valuetypes | v | valuetypes |
| vts9 | valuetypes | v | valuetypes |