Thanks for your answer Michael. On 15/10/17 06:27, michael.norr...@data61.csiro.au wrote: > This is a feature that hasn’t really been pursued. There is some code > supporting their use (akin to the way Abbr`v` is supported in calls to the > simplifier), but it is incomplete and thus unused, and pretty well > undocumented. > > But yes, the idea is to be able to label assumptions to make it easier to > refer to them in later stages of a proof. In practice, most people use the > ability to match assumptions with patterns, and/or the ability to select them > by whether or not they do or don’t raise exceptions when manipulated by rules > of inference. (For example, first_x_assum (qspec_then [`x`, `y`] mp_tac) > will only work on assumptions that are universally quantified with two > variables, and if x and y appear in the goal (which is likely), those > universal variables will have to also be of the right type.)
-- 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
