What needs to be documented? I think I just meant put an "open dep_rewrite" into bossLib.
On 22 February 2016 at 11:19, Michael Norrish <[email protected]> wrote: > Please document somewhere, but yes. > > Michael > >> On 22 Feb 2016, at 09:24, Ramana Kumar <[email protected]> wrote: >> >> So, yes? >> >> On 2 February 2016 at 15:51, Ramana Kumar <[email protected]> wrote: >>> On 2 February 2016 at 15:04, Michael Norrish <[email protected]> >>> wrote: >>>> >>>> Don't know. >>>> >>>> Is it clearly adding functionality we don't have any other way? >>> >>> >>> Yes, I think so. The other way to get the functionality is cumbersome: >>> abbreviate lots of your goal and try to instantiate the dependent rewrite >>> theorem manually. >>> >>>> >>>> >>>> Is it big (makes a difference to Moscow ML); does it contaminate the >>>> environment at all (declares new constants; adjusts grammars; adjusts other >>>> global elements of the system)? >>> >>> >>> It doesn't touch the logical environment, and I don't think it's very big. >>> >>> Implicational rewriting (issue #160) would be better, but we don't have >>> that. >>> >>>> >>>> >>>> Michael >>>> >>>> On 2 Feb 2016, at 12:17, Ramana Kumar <[email protected]> wrote: >>>> >>>> Tap tap tap... is this thing on? >>>> >>>> On 22 January 2016 at 17:56, Ramana Kumar <[email protected]> >>>> wrote: >>>>> >>>>> Would there be any harm in adding dep_rewrite to the standard set of >>>>> libraries that are loaded by default? (Similarly to how quantHeuristicsLib >>>>> was added some time recently.) >>>> >>>> >>>> >>>> ------------------------------------------------------------------------------ >>>> Site24x7 APM Insight: Get Deep Visibility into Application Performance >>>> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month >>>> Monitor end-to-end web transactions and take corrective actions now >>>> Troubleshoot faster and improve end-user experience. Signup Now! >>>> >>>> http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140_______________________________________________ >>>> Hol-developers mailing list >>>> [email protected] >>>> https://lists.sourceforge.net/lists/listinfo/hol-developers >>>> >>>> >>>> >>>> ________________________________ >>>> >>>> The information in this e-mail may be confidential and subject to legal >>>> professional privilege and/or copyright. National ICT Australia Limited >>>> accepts no liability for any damage caused by this email or its >>>> attachments. >>> >>> > > > ________________________________ > > The information in this e-mail may be confidential and subject to legal > professional privilege and/or copyright. National ICT Australia Limited > accepts no liability for any damage caused by this email or its attachments. > > ------------------------------------------------------------------------------ > Site24x7 APM Insight: Get Deep Visibility into Application Performance > APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month > Monitor end-to-end web transactions and take corrective actions now > Troubleshoot faster and improve end-user experience. Signup Now! > http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140 > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ Site24x7 APM Insight: Get Deep Visibility into Application Performance APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month Monitor end-to-end web transactions and take corrective actions now Troubleshoot faster and improve end-user experience. Signup Now! http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140 _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
