Tom Ridge wrote: > I am using EVAL to evaluate some operational semantics. EVAL often > seems to hang, when I would have expected it to simply stop. This > often seems to be the case when it doesn't know how to evaluate some > constant. Why should EVAL hang, rather than e.g. just failing?
EVAL works with equational definitions, so I'm curious how you're using it with an operational semantics. In particular, if you've made an inductive definition with Hol_reln, what equations are you using from this definition to do your evaluation? If you're using the cases (or inversion theorem), you will almost certainly be putting your system into an infinite loop. That's my best guess as to what you are seeing. Feel free to send me additional information if that doesn't cut it. Best, Michael. ------------------------------------------------------------------------- This SF.net email is sponsored by the 2008 JavaOne(SM) Conference Register now and save $200. Hurry, offer ends at 11:59 p.m., Monday, April 7! Use priority code J8TLD2. http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
