Commit 2019-05-21 16:01 34613996
View on Github →refactor(integration.lean): changing measure_space to measurable_space (#1072)
I've been using this file and range_const doesn't seem to require the spurious measure_space instance. measurable_space seems to suffice.