On 13/02/14 04:46, Vincent Aravantinos wrote:
> Then considering leaving the goal unchanged, well it is a matter of taste... I
> know it is the standard to leave the goal unchanged. But I personally met many
> buggy situations that I hardly detected because HOL {4,Light} was just
> allowing
> a rewrite (in the middle of a big script) to leave a goal unchanged whereas a
> rewrite should have happened. It was so hard to debug that I went to the
> conclusion to raise an exception instead....Note that one can transform a tactic of one type into the other with CHANGED_TAC (silently lets things not change --> exception) and TRY (exception --> silently lets things not change) Given this, I think it's probably better to have the primitives conform to the default behaviour (if only because of the principle of least surprise). Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Android apps run on BlackBerry 10 Introducing the new BlackBerry 10.2.1 Runtime for Android apps. Now with support for Jelly Bean, Bluetooth, Mapview and more. Get your Android app in front of a whole new audience. Start now. http://pubads.g.doubleclick.net/gampad/clk?id=124407151&iu=/4140/ostg.clktrk
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
