[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

Ok, it was my mistake: I was trying to use a syntax for function-valued function instead of a function of 2 arguments.  This works:

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

EXTENDS Naturals

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

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

f == h[1,2]