# 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.

## Equations

- x.out = match x with | ⟨fst, h⟩ => Classical.choose h

## Instances For

Extracts the erased value, if it is a proof.

Equivalence between `Erased α`

and `α`

.

## Equations

- Erased.equiv α = { toFun := Erased.out, invFun := Erased.mk, left_inv := ⋯, right_inv := ⋯ }

## Instances For

## Equations

- Erased.instRepr α = { reprPrec := fun (x : Erased α) (x : ℕ) => Std.Format.text "Erased" }

## Equations

- Erased.instToString α = { toString := fun (x : Erased α) => "Erased" }

Computably produce an erased value from a proof of nonemptiness.

## Equations

## Instances For

## Equations

- Erased.instInhabitedOfNonempty = { default := Erased.choice h }

@[simp]

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

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