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 uSort (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 : α), (λ (b : α), a = b) = s
def erased.mk {α : Sort u_1} :
α →

Erase a value.

Equations
• = λ (b : α), a = b, _⟩
def erased.out {α : Sort u_1} :
→ α

Extracts the erased value, noncomputably.

Equations
def erased.out_type  :
erased (Sort u)Sort u

Extracts the erased value, if it is a type.

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

Equations
theorem erased.out_proof {p : Prop} :
→ 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 α) :
= a

@[ext]
theorem erased.out_inj {α : Sort u_1} (a b : erased α) :
a.out = b.outa = b

def erased.equiv (α : Sort u_1) :
α

Equivalence between erased α and α.

Equations
@[instance]
def erased.has_repr (α : Type u) :

Equations
@[instance]
def erased.has_to_string (α : Type u) :

Equations
@[instance]
meta def erased.has_to_format (α : Type u) :

def erased.choice {α : Sort u_1} :

Computably produce an erased value from a proof of nonemptiness.

Equations
@[simp]
theorem erased.nonempty_iff {α : Sort u_1} :

@[instance]
def erased.inhabited {α : Sort u_1} [h : nonempty α] :

Equations
def erased.bind {α : Sort u_1} {β : Sort u_2} :
(α → 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 : α → ) :
a.bind f = f a.out

def erased.join {α : Sort u_1} :
erased (erased α)

Collapses two levels of erasure.

Equations
@[simp]
theorem erased.join_eq_out {α : Sort u_1} (a : erased (erased α)) :
a.join = a.out

def erased.map {α : Sort u_1} {β : Sort u_2} :
(α → β)

(<\$>) 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 α) :
a).out = f a.out

@[instance]

Equations
@[simp]
theorem erased.pure_def {α : Type u_1} :

@[simp]
theorem erased.bind_def {α β : Type u_1} :

@[simp]
theorem erased.map_def {α β : Type u_1} :

@[instance]