-
Notifications
You must be signed in to change notification settings - Fork 30
filter assign by unification #183
Copy link
Copy link
Open
Description
A convenient way to assign a hypothesis (for example, theorem.a $e |- A = ...) in metamath.exe is
assign -0 *.a
This works for most letters (not numbers because of the pm?.? series, et al)
However, a common instance where this doesn't work is for *.x, because c.x $f class .x. $. exists. In mathboxes there is also wl-impchain-com-n.m and wl-impchain-com-1.x.
But obviously class .x. and |- T. don't match with whatever assignment I'm doing. So I would like for assign to realize that these labels don't match and choose the unique one that does (theorem.x in this case).
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels