Description

Equality by convention returns true when two values are equal, and false otherwise. For some types equality is value equality and for other types equality is reference equality.

Equality is related to assignment, so after you execute
   a := b
by convention the following assertion should hold
   ~a == b

Semantics

The form
   a == b
is equivalent to
   Eq(a,b)

The form
   a ==#c b
is equivalent to
   c.sys:Eq(a,b)