Definition in coq using keyword `exists`

I'm trying to define an entity named isVector using the following syntax

Require Export Setoid.
Require Export Coq.Reals.Reals.
Require Export ArithRing.


Definition Point := Type.

Record MassPoint:Type:= cons{number : R ; point: Point}.

Variable add_MP : MassPoint -> MassPoint -> MassPoint . 

Variable mult_MP : R -> MassPoint -> MassPoint .

Variable orthogonalProjection : Point -> Point -> Point -> Point.

Definition isVector (v:MassPoint):= exists A, B :Point , v= add_MP((−1)A)(1B).

And the Coq IDE keeps complaining that there's a syntax error for the definition. Currently, I haven't figured it out.

Solution

There are many problems here.

First, you'd write:

exists A B : Point, …

with no comma between the different variables.

But then, you also have syntax errors on the right-hand side. First, I'm not sure those 1 and -1 operations exist. Second, function calls would be written this way:

add_MP A B

You can write them the way you do:

add_MP(A)(B)

But in the long run you should probably become used to the syntax of function calls being just a whitespace! You might need to axiomatize this -1 operation the way you axiomatized other operations, unless they are a notation that you defined somewhere but did not post here.