dsimp killing notations

Stream: general

[Patrick Massot]

In

import measure_theory.integral.interval_integral

open topological_space

variables {E : Type*} [normed_group E] [normed_space ℝ E]
          [complete_space E] [second_countable_topology E]
          [measurable_space E] [borel_space E]

example (f : ℝ → E) (a b : ℝ) : ∫ t in a..b, f t = 0 :=
begin
  dsimp, -- new goal is: interval_integral f a b measure_theory.measure_space.volume
  sorry
end

Does anyone understand why dsimp is killing the notation?

[Floris van Doorn]

Probably because it reduces λ t, f t to f.

[Patrick Massot]

This sounds plausible indeed. Do you see any way to prevent that?

[Patrick Massot]

Maybe we should add something like

notation `∫_` a `..` b `, ` f ` ∂` μ:70 := interval_integral f a b μ
notation `∫_` a `..` b `, ` f:70 := interval_integral f a b measure_theory.measure_space.volume

[Kyle Miller]

Does dsimp { beta := ff } prevent it?

[Kyle Miller]

It doesn't prevent it.

[Kyle Miller]

Oh, I should have paid more attention to Floris's reduction: dsimp {eta := ff} prevents it.