Here is a simple question which must have a simple answer. I have defined
a record which has the form:
rec (elt := a list, operations := Ops, ...)
where Ops := rec (...). Inside the operations are various functions defining
printing for the record, addition, and so on. I wanted to add a Length
function for these elements so I wrote a Ops.Length function which of
course doesn not work. Evidiently functions like "Print", "+" and so on
are handled differently than other functions. So how do I add a Length
function to this record?
Incidently, unless I have missed it the description of such things does not
appear to be in the manual. Similarly for the use of "arg" in function
definitions. Are these documented anywhere?
Thanks for your help,