# 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

- Erased.out x = match x with | { fst := fst, snd := h } => Classical.choose h

Extracts the erased value, if it is a type.

Note: `(mk a).OutType`

is not definitionally equal to `a`

.

## Equations

Extracts the erased value, if it is a proof.

Equivalence between `Erased α`

and `α`

.

## Equations

- Erased.equiv α = { toFun := Erased.out, invFun := Erased.mk, left_inv := (_ : ∀ (a : Erased α), Erased.mk (Erased.out a) = a), right_inv := (_ : ∀ (a : α), Erased.out (Erased.mk a) = a) }

## Equations

- Erased.instReprErased α = { reprPrec := fun x x => Std.Format.text "Erased" }

## Equations

- Erased.instToStringErased α = { toString := fun x => "Erased" }

Computably produce an erased value from a proof of nonemptiness.

## Equations

## Equations

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

`(>>=)`

operation on `Erased`

.

This is a separate definition because `α`

and `β`

can live in different
universes (the universe is fixed in `Monad`

).

## Equations

- Erased.bind a f = { fst := fun b => PSigma.fst (f (Erased.out a)) b, snd := (_ : ∃ a, (fun b => a = b) = (f (Erased.out a)).fst) }

Collapses two levels of erasure.

## Equations

- Erased.join a = Erased.bind a id

`(<$>)`

operation on `Erased`

.

This is a separate definition because `α`

and `β`

can live in different
universes (the universe is fixed in `Functor`

).

## Equations

- Erased.map f a = Erased.bind a (Erased.mk ∘ f)