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
