Report assertion errors at the assertion keyword

[keyboardDrummer]

What was changed?

When asserting a condition, do not use just condition's origin as an origin for that condition, but also the context in which it occurs. For example, let the origin be |e|nsures <expr> instead of <expr>, where the bars denote the center. This way, the origin for failing to prove the assertion is different than for failing to prove the condition's precondition, which is <expr>.

The most interesting changes are for calc statements. When the comparison between two expressions fails, the origin changes as follows. The | indicates the center and the ^s indicate the range.

Old:

  calc == {
    (x + y) * (x + y); 
    x * (x + y) + y * (x + y);
    ^^^^^^^^^^^^|^^^^^^^^^^^^
Error: the calculation step between the previous line and this line could not be proved

New:

  calc == {
    (x + y) * (x + y); 
    ^^^^^^^^^^^^^^^^^|
    x * (x + y) + y * (x + y);
    ^^^^^^^^^^^^^^^^^^^^^^^^^
Error: this calculation step could not be proved

When there is an explicit operator, it is used as the center:

  calc {
    (x + y) * (x + y);
    ^^^^^^^^^^^^^^^^^^
    ==
    |^
    x * (x + y) + y * (x + y);
    ^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: this calculation step could not be proved

How has this been tested?

• Updated existing tests

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.