Map

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) : 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