Minus sign not working, replaced by Neg.neg for now

Stream: new members

[Ilmārs Cīrulis]

import Mathlib.Data.Real.Basic

def test (x: ℝ): ℝ :=
  let another_x := x
  Neg.neg x

This works, but the following doesn't (causes error unexpected end of input:

import Mathlib.Data.Real.Basic

def test (x: ℝ): ℝ :=
  let another_x := x
  - x

[Ilmārs Cīrulis]

What am I doing wrong?

[Ruben Van de Velde]

Huh. Try (-x)

[Daniel Weber]

The second gets parsed as x - x:

import Mathlib.Data.Real.Basic

def test (x: ℝ): ℝ :=
  let another_x := x
  - x
  1

#print test

[Eric Wieser]

I would guess that using a ; after the first x also fixes it

[Eric Wieser]

I think this is worth opening an issue upstream, to track the existence of this foot gun