Hi all,
I am trying to translate some defined HOL4 functions to their equivalent
functions in SML. For instance, there is a function "exp ": real->real in a
HOL4 'transcTheory' and I want to compute it using a similar SML function
`Math.exp`.
So, I have written a translator function as follows:
fun sml_of_hol_real_exp t =
let val failstring = "Symbolic expression could not be translated in a
number" in
if fst (dest_comb t) = ``exp:real->real`` then
Math.exp <TERM TO REAL> (snd (dest_comb t))
else failwith failstring
end;
A possible usage of above function can be sml_of_hol_real_exp ``exp 0.4``;
Now, I need a kind of operator in place of <TERM TO REAL> that can give an
argument to Math.exp function for computation... Can anybody have an idea
about this?
--
Thanks and best regards,
Waqar Ahmed
------------------------------------------------------------------------------
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are
consuming the most bandwidth. Provides multi-vendor support for NetFlow,
J-Flow, sFlow and other flows. Make informed decisions using capacity
planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
