Another way of using functions

Hope allows us to use a function with two arguments like mult as an infix operator. We must assign it a priority and use it as an operator everywhere including the equations that define it. The definition of mult when used as an infix operator looks like this:

     infix mult : 8 ;
     dec mult : num # num -> num ;
     --- x mult y <= if y = 0 then 0 else x mult ( y - 1 ) + x ;
A bigger number in the infix declaration means a higher priority. The second argument of mult is parenthesised because its priority of 8 is greater than the built-in subtraction operation. Most of Hope's standard functions are supplied as infix operators.



Roger Bailey <rb@doc.ic.ac.uk>