Map

Imports

import Maybe;

Table of Contents

Types

(type)

type Map k v

Creates a new empty map.

def new : {m : (Map k v) | Map.size m = 0}

Sets the value for a key in the map.

def set (m : (Map k v)) (key : k) (value : v) : (Map k v)

Gets the value for a key in the map.

def get (m : (Map k v)) (key : k) : (Maybe v)

Gets a value with an explicit fallback of the same type.

def get_or (m : (Map k v)) (key : k) (default : v) : v

Checks if the map contains a key.

def has (m : (Map k v)) (key : k) : Bool

Removes a key from the map.

def delete (m : (Map k v)) (key : k) : (Map k v)

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

uninterpreted

Returns the size (number of entries) of the map.

def size : (m : (Map k v)) → Int