# A type for VM-erased data #

This file defines a type `Erased α`

which is classically isomorphic to `α`

,
but erased in the VM. That is, at runtime every value of `Erased α`

is
represented as `0`

, just like types and proofs.

Extracts the erased value, noncomputably.

## Instances For

Extracts the erased value, if it is a proof.

theorem
Erased.out_inj
{α : Sort u_1}
(a : Erased α)
(b : Erased α)
(h : Erased.out a = Erased.out b)
:

a = b

Computably produce an erased value from a proof of nonemptiness.

## Instances For

@[simp]

theorem
Erased.bind_eq_out
{α : Sort u_1}
{β : Sort u_2}
(a : Erased α)
(f : α → Erased β)
:

Erased.bind a f = f (Erased.out a)

@[simp]

@[simp]

theorem
Erased.map_out
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
(a : Erased α)
:

Erased.out (Erased.map f a) = f (Erased.out a)