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