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.
Instances For
Extracts the erased value, if it is a proof.
theorem
Erased.out_inj
{α : Sort u_1}
(a : Erased α)
(b : Erased α)
(h : Erased.out a = Erased.out b)
:
a = b
Computably produce an erased value from a proof of nonemptiness.
Instances For
@[simp]
theorem
Erased.bind_eq_out
{α : Sort u_1}
{β : Sort u_2}
(a : Erased α)
(f : α → Erased β)
:
Erased.bind a f = f (Erased.out a)
@[simp]
@[simp]
theorem
Erased.map_out
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
(a : Erased α)
:
Erased.out (Erased.map f a) = f (Erased.out a)