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

Equations
• = ((s : αProp) ×' ∃ (a : α), (fun (b : α) => a = b) = s)
Instances For
@[inline]
def Erased.mk {α : Sort u_1} (a : α) :

Erase a value.

Equations
• = fun (b : α) => a = b,
Instances For
noncomputable def Erased.out {α : Sort u_1} :
α

Extracts the erased value, noncomputably.

Equations
• x.out = match x with | fst, h =>
Instances For
@[reducible, inline]
abbrev Erased.OutType (a : ) :

Extracts the erased value, if it is a type.

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

Equations
• a.OutType = a.out
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 : α) :
().out = a
@[simp]
theorem Erased.mk_out {α : Sort u_1} (a : ) :
Erased.mk a.out = a
theorem Erased.out_inj {α : Sort u_1} (a : ) (b : ) (h : a.out = b.out) :
a = b
noncomputable def Erased.equiv (α : Sort u_1) :
α

Equivalence between Erased α and α.

Equations
• = { toFun := Erased.out, invFun := Erased.mk, left_inv := , right_inv := }
Instances For
instance Erased.instRepr (α : Type u) :
Repr ()
Equations
instance Erased.instToString (α : Type u) :
Equations
• = { toString := fun (x : ) => "Erased" }
def Erased.choice {α : Sort u_1} (h : ) :

Computably produce an erased value from a proof of nonemptiness.

Equations
Instances For
@[simp]
theorem Erased.nonempty_iff {α : Sort u_1} :
instance Erased.instInhabitedOfNonempty {α : Sort u_1} [h : ] :
Equations
• Erased.instInhabitedOfNonempty = { default := }
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).

Equations
• a.bind f = fun (b : β) => (f a.out).fst b,
Instances For
@[simp]
theorem Erased.bind_eq_out {α : Sort u_1} {β : Sort u_2} (a : ) (f : α) :
a.bind f = f a.out
def Erased.join {α : Sort u_1} (a : Erased ()) :

Collapses two levels of erasure.

Equations
• a.join = a.bind id
Instances For
@[simp]
theorem Erased.join_eq_out {α : Sort u_1} (a : Erased ()) :
a.join = a.out
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). Equations • = a.bind (Erased.mk f) Instances For @[simp] theorem Erased.map_out {α : Sort u_1} {β : Sort u_2} {f : αβ} (a : ) : ().out = f a.out instance Erased.Monad : Equations @[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
Equations