Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-07 22:38 e9b9014b

View on Github →

feat(data/erased): VM-erased data type

Estimated changes

added def erased.bind
added theorem erased.bind_eq_out
added def erased.choice
added def erased.join
added theorem erased.join_eq_out
added def erased.mk
added theorem erased.mk_out
added theorem erased.nonempty_iff
added theorem erased.out_mk
added theorem erased.out_proof
added def erased.out_type
added def erased
modified theorem set.mem_singleton_iff