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.

@[reducible, inline]

abbrev Erased.OutType (a : Erased (Sort u)) : Sort u

Extracts the erased value, if it is a type.

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

Equations

• a.OutType = a.out

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

Extracts the erased value, if it is a proof.

noncomputable def Erased.equiv (α : Sort u_1) : Erased α ≃ α

Equivalence between Erased α and α.

Equations

• Erased.equiv α = { toFun := Erased.out, invFun := Erased.mk, left_inv := ⋯, right_inv := ⋯ }

@[instance_reducible]

instance Erased.instRepr_mathlib (α : Type u) : Repr (Erased α)

Equations

• Erased.instRepr_mathlib α = { reprPrec := fun (x : Erased α) (x_1 : Nat) => Std.Format.text "Erased" }

@[instance_reducible]

instance Erased.instToString_mathlib (α : Type u) : ToString (Erased α)

Equations

• Erased.instToString_mathlib α = { toString := fun (x : Erased α) => "Erased" }

def Erased.choice {α : Sort u_1} (h : Nonempty α) : Erased α

Computably produce an erased value from a proof of nonemptiness.

Equations

• Erased.choice h = Erased.mk (Classical.choice h)

@[simp]

theorem Erased.nonempty_iff {α : Sort u_1} : Nonempty (Erased α) ↔ Nonempty α

@[instance_reducible]

instance Erased.instInhabitedOfNonempty_mathlib {α : Sort u_1} [h : Nonempty α] : Inhabited (Erased α)

Equations

• Erased.instInhabitedOfNonempty_mathlib = { default := Erased.choice h }

def Erased.bind {α : Sort u_1} {β : Sort u_2} (a : Erased α) (f : α → Erased β) : Erased β

(>>=) operation on Erased.

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

Equations

• a.bind f = ⟨fun (b : β) => ↑(f a.out) b, ⋯⟩

@[simp]

theorem Erased.bind_eq_out {α : Sort u_1} {β : Sort u_2} (a : Erased α) (f : α → Erased β) : a.bind f = f a.out

def Erased.join {α : Sort u_1} (a : Erased (Erased α)) : Erased α

Collapses two levels of erasure.

Equations

• a.join = a.bind id

@[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 α) : Erased β

(<$>) operation on Erased.

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

Equations

• Erased.map f a = a.bind (Erased.mk ∘ f)

@[simp]

theorem Erased.map_out {α : Sort u_1} {β : Sort u_2} {f : α → β} (a : Erased α) : (map f a).out = f a.out

@[instance_reducible]

instance Erased.Monad : Monad Erased

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Erased.pure_def {α : Type u_1} : pure = mk

@[simp]

theorem Erased.bind_def {α β : Type u_1} : (fun (x1 : Erased α) (x2 : α → Erased β) => x1 >>= x2) = bind

@[simp]

theorem Erased.map_def {α β : Type u_1} : (fun (x1 : α → β) (x2 : Erased α) => x1 <$> x2) = map

instance Erased.instLawfulMonad : LawfulMonad Erased