I'd say a big difference is that irule can only be used as a tactic,
whereas MP_CANON is a rule that can be used in more general situations.
Could the technology inside irule be split out into a rule or conversion,
or is it essentially a tactic?
On 17 November 2015 at 00:39, Jeremy Dawson <jeremy.daw...@anu.edu.au>
wrote:
> Hi Ramana,
>
> Well, they are both ways of matching the final consequent of a1 ==> a2
> ==> a3 ==> ... ==> c with the goal.
>
> Until I saw your question I hadn't been aware of the existence of
> MP_CANON.
>
> Possibly the biggest difference is that irule will produce multiple new
> subgoals (eg, in the above case, one for each ai - except as noted below).
>
> There's a bit of reimplementation of irule recently and continuing,
> involving the behaviour when there are variables some of the ai but not
> in c, (like MATCH_MP_TAC, it introduces existentials, which also may
> require collecting together some of the ai) which may affect ordering
> and exact form of the new subgoals.
>
> Cheers,
>
> Jeremy
>
>
>
> On 16/11/15 22:28, Ramana Kumar wrote:
> > What is the difference between irule and (match_mp_tac o MP_CANON)?
> >
> > I'm more interested in differences in the intended design than in minor
> > details in the implementation. Which is preferred style? Which should
> > get more developer time?
> >
> > Maybe they're actually rather different, but as far as I saw, from a
> > brief look, they are intended to do the same thing.
> >
> >
> >
> ------------------------------------------------------------------------------
> > Presto, an open source distributed SQL query engine for big data,
> initially
> > developed by Facebook, enables you to easily query your data on Hadoop
> in a
> > more interactive manner. Teradata is also now providing full enterprise
> > support for Presto. Download a free open source copy now.
> > http://pubads.g.doubleclick.net/gampad/clk?id=250295911&iu=/4140
> >
> >
> >
> > _______________________________________________
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
>
>
> ------------------------------------------------------------------------------
> Presto, an open source distributed SQL query engine for big data, initially
> developed by Facebook, enables you to easily query your data on Hadoop in a
> more interactive manner. Teradata is also now providing full enterprise
> support for Presto. Download a free open source copy now.
> http://pubads.g.doubleclick.net/gampad/clk?id=250295911&iu=/4140
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Go from Idea to Many App Stores Faster with Intel(R) XDK
Give your users amazing mobile app experiences with Intel(R) XDK.
Use one codebase in this all-in-one HTML5 development environment.
Design, debug & build mobile apps & 2D/3D high-impact games for multiple OSs.
http://pubads.g.doubleclick.net/gampad/clk?id=254741551&iu=/4140
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
