Either

Imports
open Copy;
Table of Contents

Types

Either

(inductive)
inductive Either a b

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.

Either (inductive)

left

constructor
(Either a b)

right

constructor
(Either a b)

Functions

either

def either (f : (x : a) → c) (g : (x : b) → c) (value : (Either a b)) : c

map

def map (f : (x : b) → c) (value : (Either a b)) : (Either a c)