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
The 7th International Conference on Interactive Theorem Proving
22 to 27 August 2016 in Nancy, France
https://itp2016.inria.fr
Early registration deadline: 30 June
Main conference: 22 August to 25 August (morning)
Affiliated events: 25 August (afternoon) to 27 August
ITP is the premier
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
