Hi Naeem,
1. "op" is not the keyword to use. Instead, use either
the "dollar" notation (thus, "$+" or "arithmetic$+"), or the
"paren" notation "(+)", which is also supported.
2. FOLD on sets is already defined: it is called ITSET.
See the Description (page 102) for a short descriptio
Hello,
I am trying to define a function named SETSUM which uses another
function FOLD:
(FOLD)
- val FOLD_defn = Defn.Hol_defn
"FOLD"
`FOLD (f:'a->'a->'a) (g:'b->'a) (z:'a) (A:'a->bool) =
if FINITE A then if A={} then z else FOLD f g (CHOICE
