This operation allows arbitrary information or comments to be embedded
in a virtual code application in such a way that it will be ignored by
avram when executing it. For the silly language, a
note function is defined in the standard prelude so as to imply
the following theorem.
note]] (f,c) = ((nil,nil),((nil,nil),(nil,(nil,(f,c)))))
Intuitively, the argument f represents a function, and the
argument c represents the comment, annotation, or whatever, that
will be embedded but ignored in the virtual code.
Semantically, a function with a note attached is the same as the
function by itself, as the following property stipulates for
any non-nil f.
note]] (f,c)) x = f x
A possible reason for using this feature might be to support a language that performs run-time type checking by hanging type tags on everything. Another possible use would be to include symbolic information needed by a debugger.