Unknown operator: 'account_total'

[vjocw]

Hi, I'm going through this example:

https://learntla.com/introduction/example/

but I cannot get the IDE to parse account total. I copied and pasted the example.

variables alice_account = 10, bob_account = 10, money \in 1..20,
          account_total = alice_account + bob_account;

begin
Transfer:
  if alice_account >= money then
    A: alice_account := alice_account - money;
       bob_account := bob_account + money; \* Both now part of A
end if;
C: assert alice_account >= 0;

end algorithm *)

\* BEGIN TRANSLATION
\* removed..
\* END TRANSLATION

MoneyNotNegative == money >= 0
MoneyInvariant == alice_account + bob_account = account_total

[vjocw]

solved the issue by restarting the IDE