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 (max1u)

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
@[inline]
def Erased.mk {α : Sort u_1} (a : α) :

Erase a value.

Equations
  • Erased.mk a = { fst := fun b => a = b, snd := (_ : a, (fun b => a = b) = fun b => a = b) }
noncomputable def Erased.out {α : Sort u_1} :
Erased αα

Extracts the erased value, noncomputably.

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

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

Extracts the erased value, if it is a proof.

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

Equivalence between Erased α and α.

Equations
instance Erased.instReprErased (α : Type u) :
Equations
Equations
def Erased.choice {α : Sort u_1} (h : Nonempty α) :

Computably produce an erased value from a proof of nonemptiness.

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

(>>=) operation on Erased.

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

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

Collapses two levels of erasure.

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

(<$>) operation on Erased.

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

Equations
@[simp]
theorem Erased.map_out {α : Sort u_1} {β : Sort u_2} {f : αβ} (a : Erased α) :
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