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.)
Michael
On 15/10/17, 02:54, "Mario Castelán Castro" <marioxcc...@yandex.com> wrote:
Hello.
What is the purpose of labels? The ones from the theory “marker”: “$:-”.
I see that there are some functions in src/marker/markerLib.sml that
suggest these are used to designate labels on assumptions. Is this
documented somewhere?
Thanks.
--
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
------------------------------------------------------------------------------
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
