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.
Extracts the erased value, noncomputably.
Equations
- erased.out ⟨s, h⟩ = classical.some h
Extracts the erased value, if it is a proof.
Equivalence between erased α and α.
Equations
- erased.equiv α = {to_fun := erased.out α, inv_fun := erased.mk α, left_inv := _, right_inv := _}
@[instance]
Equations
- erased.has_repr α = {repr := λ (_x : erased α), "erased"}
@[instance]
Equations
- erased.has_to_string α = {to_string := λ (_x : erased α), "erased"}
Computably produce an erased value from a proof of nonemptiness.
Equations
@[instance]
Equations
@[simp]
theorem
erased.map_out
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
(a : erased α) :
(erased.map f a).out = f a.out
@[instance]