Implicit functions: currying and totality

Question

When specifying an implicit function in VDM-SL, is it possible to specify a curried function? In the following test1 and test2 are explicit uncurried and curried functions, and test3 is an implicit uncurried function. All are accepted by Overture. test4 is an attempt at an implicit curried function, but it is rejected by Overture.

Also, is there any way to specify with an implicit function definition that it should be total?

module moduleName
  exports all
  definitions
  functions

  test1 : nat * nat +> nat
  test1 (arg1,arg2) == arg1+arg2;

  test2 : nat -> nat +> nat
  test2 (arg1) (arg2) == arg1+arg2;

  test3 (arg1:nat,arg2:nat) res:nat
  post res = arg1+arg2;

  test4 (arg1:nat) (arg2:nat) res:nat
  post res = arg1+arg2;

end moduleName

Answer 1

No, I'm afraid curried functions are only provided for explicit function definitions. And there is no partial/total indicator for implicit definitions.

(I just asked why we have this difference. It seems it is to do with the history of the language: the English school produced implicit functions but without currying, whereas the Danish school had explicit functions with currying. They ought really to be harmonized - and your guessed syntax would probably be the result.)