Modules

type
Map
(
'key
, 
'order
)
=
{ 
∀ 'val.
ordered_map
(
'key
, 
'val
, 
'order
)
 
empty
, 
∀ 'val.
(
'key
, 
'val
ordered_map
(
'key
, 
'val
, 
'order
)
)
 
singleton
, 
∀ 'val.
(
ordered_map
(
'key
, 
'val
, 
'order
)
bool
)
 
is_empty
, 
∀ 'val.
(
'key
, 
'val
, 
ordered_map
(
'key
, 
'val
, 
'order
)
ordered_map
(
'key
, 
'val
, 
'order
)
)
 
add
, 
∀ 'val.
(
'key
, 
'val
, 
ordered_map
(
'key
, 
'val
, 
'order
)
option
(
ordered_map
(
'key
, 
'val
, 
'order
)
)
)
 
add_without_erasing
, 
∀ 'val.
(
'key
, 
ordered_map
(
'key
, 
'val
, 
'order
)
option
(
'val
)
)
 
get
, 
∀ 'val.
(
'key
, 
ordered_map
(
'key
, 
'val
, 
'order
)
option
(
{ 
'key
 
key
, 
'val
 
val
 }
)
)
 
get_key_val
, 
∀ 'val.
(
(
'key
, 
'val
bool
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
option
(
{ 
'key
 
key
, 
'val
 
val
 }
)
)
 
find
, 
∀ 'acc, 'val.
(
(
'key
, 
'val
, 
'acc
'acc
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
, 
'acc
'acc
)
 
fold
, 
∀ 'acc, 'val.
(
(
'key
, 
'val
, 
'acc
'acc
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
, 
'acc
'acc
)
 
rev_fold
, 
∀ 'acc, 'val.
(
(
int
, 
'key
, 
'val
, 
'acc
'acc
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
, 
'acc
'acc
)
 
foldi
, 
∀ 'acc, 'val.
(
(
int
, 
'key
, 
'val
, 
'acc
'acc
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
, 
'acc
'acc
)
 
rev_foldi
, 
∀ 'val.
(
(
'key
, 
'val
bool
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
ordered_map
(
'key
, 
'val
, 
'order
)
)
 
filter
, 
∀ 'new_value, 'value.
(
(
'value
option
(
'new_value
)
)
, 
ordered_map
(
'key
, 
'value
, 
'order
)
ordered_map
(
'key
, 
'new_value
, 
'order
)
)
 
filter_map
, 
∀ 'new_val, 'val.
(
(
'val
'new_val
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
ordered_map
(
'key
, 
'new_val
, 
'order
)
)
 
map
, 
∀ 'new_val, 'val.
(
(
'key
, 
'val
'new_val
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
ordered_map
(
'key
, 
'new_val
, 
'order
)
)
 
mapi
, 
∀ 'val.
(
(
'key
, 
'val
void
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
void
)
 
iter
, 
∀ 'val.
(
ordered_map
(
'key
, 
'val
, 
'order
)
(
'key
, 
'val
)
)
 
min_binding
, 
∀ 'val.
(
ordered_map
(
'key
, 
'val
, 
'order
)
(
'key
, 
'val
)
)
 
max_binding
, 
∀ 'val.
(
'key
, 
ordered_map
(
'key
, 
'val
, 
'order
)
bool
)
 
contains
, 
∀ 'val.
(
'key
, 
ordered_map
(
'key
, 
'val
, 
'order
)
bool
)
 
mem
, 
∀ 'val.
(
ordered_map
(
'key
, 
'val
, 
'order
)
int
)
 
size
, 
∀ 'val.
(
ordered_map
(
'key
, 
'val
, 
'order
)
int
)
 
height
, 
∀ 'val.
(
(
'val
, 
'val
Order.comparison
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
Order.comparison
)
 
compare
, 
∀ 'val.
(
(
'val
, 
'val
Order.ordering
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
Order.ordering
)
 
order_maps
, 
∀ 'value.
(
(
'key
, 
'value
bool
)
, 
ordered_map
(
'key
, 
'value
, 
'order
)
bool
)
 
exists
, 
∀ 'val.
(
(
'key
, 
'val
bool
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
list
(
(
'key
, 
'val
)
)
)
 
retrieve
, 
∀ 'val.
(
'key
, 
(
'val
'val
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
ordered_map
(
'key
, 
'val
, 
'order
)
)
 
replace
, 
∀ 'val.
(
'key
, 
(
option
(
'val
)
'val
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
ordered_map
(
'key
, 
'val
, 
'order
)
)
 
replace_or_add
, 
∀ 'val.
(
ordered_map
(
'key
, 
'val
, 
'order
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
ordered_map
(
'key
, 
'val
, 
'order
)
)
 
union
, 
∀ 'val.
(
ordered_map
(
'key
, 
'val
, 
'order
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
ordered_map
(
'key
, 
'val
, 
'order
)
)
 
intersection
, 
∀ 'val.
(
'key
, 
ordered_map
(
'key
, 
'val
, 
'order
)
(
ordered_map
(
'key
, 
'val
, 
'order
)
, 
option
(
'val
)
)
)
 
extract
, 
∀ 'val.
(
ordered_map
(
'key
, 
'val
, 
'order
)
(
ordered_map
(
'key
, 
'val
, 
'order
)
, 
option
(
(
'key
, 
'val
)
)
)
)
 
extract_min_binding
, 
∀ 'val.
(
ordered_map
(
'key
, 
'val
, 
'order
)
(
ordered_map
(
'key
, 
'val
, 
'order
)
, 
option
(
(
'key
, 
'val
)
)
)
)
 
extract_max_binding
, 
∀ 'val.
(
ordered_map
(
'key
, 
'val
, 
'order
)
option
(
(
'key
, 
'val
)
)
)
 
random_get
, 
∀ 'val.
(
(
'key
bool
)
, 
(
'key
bool
)
, 
ordered_map
(
'key
, 
'val
, 
'order
)
ordered_map
(
'key
, 
'val
, 
'order
)
)
 
sub_map_gen
, 
∀ 'val.
(
'key
, 
'key
, 
ordered_map
(
'key
, 
'val
, 
'order
)
ordered_map
(
'key
, 
'val
, 
'order
)
)
 
submap
, 
∀ 'val.
(
'key
, 
ordered_map
(
'key
, 
'val
, 
'order
)
ordered_map
(
'key
, 
'val
, 
'order
)
)
 
greater
, 
∀ 'val.
(
'key
, 
ordered_map
(
'key
, 
'val
, 
'order
)
ordered_map
(
'key
, 
'val
, 
'order
)
)
 
lesser
, 
∀ 'val.
(
'key
, 
ordered_map
(
'key
, 
'val
, 
'order
)
ordered_map
(
'key
, 
'val
, 
'order
)
)
 
remove
, 
{ 
∀ 'val.
(
list
(
(
'key
, 
'val
)
)
ordered_map
(
'key
, 
'val
, 
'order
)
)
 
assoc_list
 }
 
From
, 
{ 
∀ 'val.
(
ordered_map
(
'key
, 
'val
, 
'order
)
list
(
(
'key
, 
'val
)
)
)
 
assoc_list
, 
∀ 'val.
(
ordered_map
(
'key
, 
'val
, 
'order
)
list
(
'key
)
)
 
key_list
, 
∀ 'val.
(
ordered_map
(
'key
, 
'val
, 
'order
)
list
(
'val
)
)
 
val_list
, 
∀ 'val.
(
ordered_map
(
'key
, 
'val
, 
'order
)
iter
(
(
'key
, 
'val
)
)
)
 
iter
, 
∀ 'val.
(
ordered_map
(
'key
, 
'val
, 
'order
)
iter
(
(
'key
, 
'val
)
)
)
 
rev_iter
 }
 
To
 }
type
intmap
(
β
)
=
type
map
(
'key
, 
'val
)
=
type
ordered_map
(
'key
, 
'val
, 
'order
)
type =
Name Summary
A on numbers, using numeric comparison.
Map
The default module.Chances are that you will use this module for most tasks. It uses the default co...
A on strings, using alphabetical comparison on strings.This instance of differentiates uppercase f...

Comments

The browser you use is not supported by this application, probably because it lacks some critical features.
For a better experience, please consider using this application with a supported browser.