I think that function is DB.find (PolyML and therefore HOL4 has separate
namespaces due to the module system).
You can ask the help system about it:
help "find";
which will bring up a menu listing all structures known to the help system
that have a "find" function in their signature. As
Hi Ada,
you can't print the definition from the ML REPL. I expect you use
PolyML. In this case look into the file "POLYML_DIR/basis/List.sml".
There you will find the following definition.
fun find _ [] = NONE
| find f (a::b) = if f a then SOME a else find f b
Best
Thomas
On 21.06.2016 11:18,
Hi,guys
I am working with HOL4.
I finded a function "find" in ML Structure list,and I wanted to see the
function body of "find". I printed :
- find;
> > val it = fn : string -> ((string * string) * (thm * class)) list
The result only shows the types of the function.
Its
