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
