Dependencies

plugin core;

plugin option;

Types

Key

This existential-style type specifies a type together with a less-than function.

anx let Key = [T: *, lt: [T, T] → Bool];

Set / Map

Type constructors for set / map.

First argument must be of type ord.Key.
ord.Map needs a second argument: the value type.

axm Set: Key → *;

axm Map: Key → * → *;

Constructors

init

Creates a set / map from a list of values / key-value pairs.

pub mod init {
    axm set: [K: Key] →          {n: Nat} → «n;  K#T    » → Set K  , normalize_init;
    axm map: [K: Key] → {V: *} → {n: Nat} → «n; [K#T, V]» → Map K V, normalize_init;
}

create

Creates an empty set / map.

anx lam create_set (K: Key) : Set K = init.set K @0 ();

anx lam create_map (K: Key) (V: *) : Map K V = init.map K @V @0 ();

Capacity

size

Yields the number of elements in the container.

pub mod size {
    axm set: {K: Key} →          Set K   → Nat, normalize_size;
    axm map: {K: Key} → {V: *} → Map K V → Nat, normalize_size;
}

is_empty

Is the container empty?

anx lam is_empty_set {K: Key} (set: Set K ): Bool = core.ncmp.e (size.set set, 0);

anx lam is_empty_map {K: Key} {V: *} (map: Map K V): Bool = core.ncmp.e (size.map map, 0);

Lookup

get

Looks up the given key in the map. Returns an optional value (option.Opt V).

axm get: {K: Key} → {V: *} → [Map K V, K#T] → option.Opt V, normalize_get;

contains

Does the container contain the given key?

pub mod contains {
    axm set: {K: Key} →          [Set K  , K#T] → Bool, normalize_contains;
    axm map: {K: Key} → {V: *} → [Map K V, K#T] → Bool, normalize_contains;
}

Modifiers

insertion

Inserts a key / key-value pair into the container.

pub mod insertion {
    axm set: {K: Key} →          [Set K  ,  K#T    ] → Set K  , normalize_insert;
    axm map: {K: Key} → {V: *} → [Map K V, [K#T, V]] → Map K V, normalize_insert;
}