Interval integral

Stream: mathlib4

[Patrick Massot]

What is new idiomatic way to write $\int_0^1 x\,dx$? I know ∫ x in (0 : ℝ)..1, x works, but is doesn't look nice.

[Kyle Miller]

I haven't tested it, but you could try ∫ x : ℝ in 0..1, x, which looks a little nicer

[Patrick Massot]

I should have written this was my first attempt, but it doesn't work.

[Patrick Massot]

type mismatch
  0..val
has type
  floatSpec.float : Type
but is expected to have type
  Set ℝ : Type

[Patrick Massot]

It really feels like something is missing a scope. Things about float shouldn't interfere here.

[Henrik Böving]

I think this is a funny interaction of builtin syntax. 0. is a shorthand for 0.0 : Floatlike in many other languages and .val is the dot notation val operation on float

[Kyle Miller]

So perhaps ∫ x : ℝ in 0 .. 1, x might work?

[Arend Mellendijk]

It doesn't, but ∫ x in (0)..1, x does.

[Patrick Massot]

For 10 very weird seconds it seemed that everything worked, including ∫ x in 0 .. 1, x. Then I realized I was working in the wrong VSCode, the one running Lean 3 :(

[Patrick Massot]

I guess it's time for me to take a break.

[Yury G. Kudryashov]

I think that this issue with zero is a good reason to change the notation.

[Yury G. Kudryashov]

See this thread

[Yury G. Kudryashov]

I failed to implement the ∫ x in [a:b], f x notation from there.