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.

Equations
• = Σ' (s : α → Prop), ∃ (a : α), (λ (b : α), a = b) = s
def erased.mk {α : Sort u_1} (a : α) :

Erase a value.

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

Extracts the erased value, noncomputably.

Equations
def erased.out_type (a : 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} (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 α) :
= a
@[ext]
theorem erased.out_inj {α : Sort u_1} (a b : erased α) (h : a.out = b.out) :
a = b
noncomputable def erased.equiv (α : Sort u_1) :
α

Equivalence between erased α and α.

Equations
@[protected, instance]
def erased.has_repr (α : Type u) :
Equations
@[protected, instance]
def erased.has_to_string (α : Type u) :
Equations
@[protected, instance]
meta def erased.has_to_format (α : Type u) :
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} :
@[protected, instance]
def erased.inhabited {α : Sort u_1} [h : nonempty α] :
Equations
def erased.bind {α : Sort u_1} {β : Sort u_2} (a : erased α) (f : α → ) :

(>>=) 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} (a : 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} (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 α) :
a).out = f a.out
@[protected, 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} :
@[protected, instance]