Michael Leuschel

Maybe you can also try and install our new nightly build first; we have extended the error log output. Nightly builds of ProB for Rodin 3 can be obtained from within Rodin by using the update site https://stups.hhu-hosting.de/rodin/prob1/nightly.

It would also be interesting to know which version of Rodin and which version of the ProB for Rodin plugin you used. I guess you are running Rodin on Windows?

Dear Steve, the syntax I wrote was classical B; in Rodin you have to write the lambda slightly differently: context ifte_wd_test constants x c axioms @axm0 x=0 @axm1 c = ((λdummy·dummy=0 ∧ x>0∣1÷x) ∪ (λdummy·dummy =0 ∧ ¬(x>0)∣0)) (0) theorem @thm1 c=0 end The WD PO is proven automatically. Michael PS: The lambda translation was introduced by Dominik Hansen in the translation of TLA+ to B; TLA+ has an if-then-else for expressions. On 28 Feb 2019, at 14:37, Michael Leuschel mleuschel@users.sourceforge.net...

Dear Steve You can also write something like (%(dummy).(dummy=0 & x>0|1/x)\/%(dummy).(dummy =0 & not(x>0)|0)) (0) instead of {TRUE ↦ 1÷x, FALSE ↦ 0}(bool(x ≠ 0)) The lambda construction is well-defined (but not very readable by a human) and ProB transforms this form internally into an expression (IF x > 0 THEN 1 ÷ x ELSE 0 END) Greetings, Michael On 28 Feb 2019, at 13:33, Laurent Voisin lvoisin@users.sourceforge.net wrote: For instance, writing {TRUE ↦ 1÷x, FALSE ↦ 0}(bool(x ≠ 0)) is ill-defined...

Rodin 3.2 seems to have the same issue on Mac OS X High Sierra. We have the same issue on the other laptop with High Sierra installed on it: all hypotheses are just white and the goal is only partially readable. It also seems that saving a file does not always trigger the Rodin builder, in particular when the builder is still running for a previous change. (But I am not entirely sure about this issue.)

Proof view: unreadable formulas (white on white)

Tactic Profile Editing very slow performance

Event Wizard Add Button Fields Disappear