Camelia, the Perl 6 bug

IRC log for #isabelle, 2011-12-05

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
02:06 monochrom joined #isabelle
15:45 phimuemue_ joined #isabelle
19:23 bwright joined #isabelle
23:14 dschoepe joined #isabelle
23:16 dschoepe How can I ask Isabelle to compute the value of a (possibly) non-terminating function (defined via `function')? (I did not do the termination proof, and running `value foo' directly afterwards, does not reduce the function call)
23:35 larsrh dschoepe: have you tried defining an inductive instead?
23:35 larsrh you can run "code_pred" and afterwards "values"
23:36 dschoepe larsrh: Ah, thanks. The function was actually an eval-function for an inductively defined toy-language semantics.
23:38 larsrh I didn't do any termination proofs yet, but defining possibly non-terminating functions as inductives always worked fine for me so far.
23:41 dschoepe Well, I'm sure the function in question doesn't terminate in general, but I'd like isabelle to try evaluating it for some arguments anyway (for which it should terminate) anyway.
23:44 wagle joined #isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary