Commit 2022-12-20 15:25 27379733

View on Github →

feat port: Data.Erased (#937) 10b4e499f43088dd3bb7b5796184ad5216648ab1 One instance at the end is a bit longer because we don't have refine' { .. }. No other issues

Estimated changes

added def Erased.OutType
added def Erased.bind
added theorem Erased.bind_def
added theorem Erased.bind_eq_out
added def Erased.choice
added def Erased.join
added theorem Erased.join_eq_out
added def Erased.map
added theorem Erased.map_def
added theorem Erased.map_out
added def Erased.mk
added theorem Erased.mk_out
added theorem Erased.nonempty_iff
added theorem Erased.out_inj
added theorem Erased.out_mk
added theorem Erased.out_proof
added theorem Erased.pure_def
added def Erased