def Erased (α : Sort u) : Sort (max 1 u)

A value hidden from compiled code. Erased.mk 42 erases to a dummy at runtime, and proofs recover the 42 as (Erased.mk 42).out.

Equations

• Erased α = { s : α → Prop // ∃ (a : α), (fun (x : α) => a = x) = s }

@[macro_inline]

def Erased.mk {α : Sort u} (a : α) : Erased α

Hides a in an Erased α. Compiled code drops the argument.

Equations

• Erased.mk a = ⟨fun (b : α) => a = b, ⋯⟩

noncomputable def Erased.out {α : Sort u} (e : Erased α) : α

The value hidden in e, available to proofs only.

Equations

• e.out = Classical.choose ⋯

@[simp]

theorem Erased.out_mk {α : Sort u} (a : α) : (mk a).out = a

@[simp]

theorem Erased.mk_out {α : Sort u} (e : Erased α) : mk e.out = e

theorem Erased.out_inj {α : Sort u} {a b : Erased α} (h : a.out = b.out) : a = b

theorem Erased.out_inj_iff {α : Sort u} {a b : Erased α} : a = b ↔ a.out = b.out

@[simp]

theorem Erased.mk_inj {α : Sort u} {a b : α} : mk a = mk b ↔ a = b