# Documentation

Mathlib.Data.Erased

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

def Erased (α : Sort u) :
Sort (max 1 u)

Erased α is the same as α, except that the elements of Erased α are erased in the VM in the same way as types and proofs. This can be used to track data without storing it literally.

Instances For
@[inline]
def Erased.mk {α : Sort u_1} (a : α) :

Erase a value.

Instances For
noncomputable def Erased.out {α : Sort u_1} :
α

Extracts the erased value, noncomputably.

Instances For
@[reducible]
def Erased.OutType (a : Erased (Sort u)) :

Extracts the erased value, if it is a type.

Note: (mk a).OutType is not definitionally equal to a.

Instances For
theorem Erased.out_proof {p : Prop} (a : ) :
p

Extracts the erased value, if it is a proof.

@[simp]
theorem Erased.out_mk {α : Sort u_1} (a : α) :
= a
@[simp]
theorem Erased.mk_out {α : Sort u_1} (a : ) :
= a
theorem Erased.out_inj {α : Sort u_1} (a : ) (b : ) (h : ) :
a = b
noncomputable def Erased.equiv (α : Sort u_1) :
α

Equivalence between Erased α and α.

Instances For
instance Erased.instReprErased (α : Type u) :
Repr ()
def Erased.choice {α : Sort u_1} (h : ) :

Computably produce an erased value from a proof of nonemptiness.

Instances For
@[simp]
theorem Erased.nonempty_iff {α : Sort u_1} :
instance Erased.instInhabitedErased {α : Sort u_1} [h : ] :
def Erased.bind {α : Sort u_1} {β : Sort u_2} (a : ) (f : α) :

(>>=) operation on Erased.

This is a separate definition because α and β can live in different universes (the universe is fixed in Monad).

Instances For
@[simp]
theorem Erased.bind_eq_out {α : Sort u_1} {β : Sort u_2} (a : ) (f : α) :
= f ()
def Erased.join {α : Sort u_1} (a : Erased ()) :

Collapses two levels of erasure.

Instances For
@[simp]
theorem Erased.join_eq_out {α : Sort u_1} (a : Erased ()) :
def Erased.map {α : Sort u_1} {β : Sort u_2} (f : αβ) (a : ) :

(<$>) operation on Erased. This is a separate definition because α and β can live in different universes (the universe is fixed in Functor). Instances For @[simp] theorem Erased.map_out {α : Sort u_1} {β : Sort u_2} {f : αβ} (a : ) : Erased.out () = f () @[simp] theorem Erased.pure_def {α : Type u_1} : pure = Erased.mk @[simp] theorem Erased.bind_def {α : Type u_1} {β : Type u_1} : (fun x x_1 => x >>= x_1) = Erased.bind @[simp] theorem Erased.map_def {α : Type u_1} {β : Type u_1} : (fun x x_1 => x <$> x_1) = Erased.map