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 follows:
h> elp "find";
--------------------------------------------------
| 1 | val PIntMap.find |
| 2 | val LVTermNet.find |
| 3 | val Redblackmap.find |
| 4 | val KernelSig.find |
| 5 | val Redblackset.find |
| 6 | val Intset.find |
| 7 | val TypeNet.find |
| 8 | val DB.find |
| 9 | val mlibPatricia.find |
| 10 | HOL DB.find (help/Docfiles/DB.find.adoc) |
| 11 | val mlibSolver.find |
--------------------------------------------------
Choose number to browse, or quit: 10
+ ----------------------------------------------------------------------
+ find (DB)
+ ----------------------------------------------------------------------
+ find : string -> data list
+
+ SYNOPSIS
+ Search for theory element by name fragment.
+
On Tue, Jun 21, 2016 at 4:29 AM, Thomas Tuerk <tho...@tuerk-brechen.de>
wrote:
> 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, Ada wrote:
> > 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 description in ML library is:
> > [*find* p xs] applies f to each element x of xs, from left to right
> > until p(x) evaluates to true; returns SOME x if such an x exists
> > otherwise NONE.
> > But,the function body or the definition of function doesn't exist.
> > Does anyone know how to show the function body ?
> > Thanks!
> >
> >
> >
> ------------------------------------------------------------------------------
> > Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
> > Francisco, CA to explore cutting-edge tech and listen to tech luminaries
> > present their vision of the future. This family event has something for
> > everyone, including kids. Get more information and register today.
> > http://sdm.link/attshape
> >
> >
> >
> > _______________________________________________
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
>
>
> ------------------------------------------------------------------------------
> Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
> Francisco, CA to explore cutting-edge tech and listen to tech luminaries
> present their vision of the future. This family event has something for
> everyone, including kids. Get more information and register today.
> http://sdm.link/attshape
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
