Copy

Values that can be duplicated without creating aliases to unique resources. An instance promises ordinary unrestricted reuse is safe. Linear handles deliberately have no instances; move them with consuming operations instead.
Table of Contents

Types

Copy

(inductive)
Values that can be duplicated without creating aliases to unique resources. An instance promises ordinary unrestricted reuse is safe. Linear handles deliberately have no instances; move them with consuming operations instead.
inductive Copy a

Constructors

For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.

Copy (inductive)

mk

constructor
Values that can be duplicated without creating aliases to unique resources. An instance promises ordinary unrestricted reuse is safe. Linear handles deliberately have no instances; move them with consuming operations instead.
(Copy a)

Functions

duplicate

def duplicate ∀a:Β (_d1404 : (Copy a)) (x : a) : {r : a | r = x}