n applying the function [m \in Nat, n \in Nat |-> the argument list is: 1

[Y2i <yur...@xxxxxxxxx>]

Good evening,

When I try to evaluate r in Model -> Model Checking Results -> Evaluated Constant _expression_, I'm getting the following error:

The `Evaluate Constant _expression_? section?s evaluation failed.

In applying the function

[m \in Nat, n \in Nat |-> <_expression_ line 4, col 32 to line 4, col 36 of module Calc>],

the argument list is:

1

which does not match its formal parameter.

If I replace r == h[1,2] with r == e[1,2], everything works.  

What is wrong with definition of h?

Thank you,

Yuri

-------------------------------- MODULE Calc --------------------------------

EXTENDS Naturals

e == [m \in Nat, n \in Nat |-> m + n]

h == [e EXCEPT ![1][2] = 0]

r == h[1,2]

=============================================================================