Hello Thomas. On 25/09/17 14:18, Thomas Tuerk wrote: > I believe, there is nothing bad about using inline functions (i.e. a > lambda) per se. If I understood correctly, you are currently using the > following from […]
Indeed that is what I am using. > A slightly more elegant way might be (it's all a matter of opinion :-)) […] Oh, right. I know about Q.SUBGOAL_THEN but I had not thought about using it for this purpose. > However, this keeps the inline function. I don't know of a SUBST1_TAC > like function. However, it is easy to define. You could use REWR_CONV > (or it's higher order corresponding function) and combine it with > tacticals. You would end up with something like […] Thanks!. -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
