Thank you. This works. On Tuesday, February 6, 2024 at 1:32:21 AM UTC-5 [email protected] wrote:
> If I correctly understand the issue, then a feature similar to what you > described already exists in Metamath-lamp. In order to change a > justification, you may do the following: > > 1. Select the checkbox to the left of the step you want to modify the > justification for. > 2. > > Click the “Unify all” button. > 3. > > In the text field “Label of root justification” select another > assertion you want to use. It is enough to type only a part of another > assertion name. > 4. > > If the new assertion requires another set of arguments, then make sure > the parameter “Allowed statements: first level” is set to “All”. If the > arguments are the same, then you may leave this parameters as is. > 5. > > Click the “Prove” button. > 6. > > If a proof is found then clicking the “Apply” button will modify the > justification in the editor to use the new assertion you selected. > > > Here is a short demo - > https://drive.google.com/file/d/1R4waaGFS2WUT-Apq7RMXVuaUIJMVhh8q/view?usp=sharing > > > – > > Igor > > On Tuesday, February 6, 2024 at 12:04:56 AM UTC+1 [email protected] > wrote: > >> Hi all. >> >> I'm in the process of writing my own Metamath database. To start, it's >> basically a refactoring of the logic portion of the set.mm database but >> with my own numbered naming system for theorems in order to correspond with >> a pdf book that explains things informally but in more detail. Anyways I >> will share more later if anyone is interested. >> >> My main issue is when writing proofs I sometimes wish to use a specific >> theorem for the sake of clarity, but the proof assistant will automatically >> complete the proof with a different theorem. This happens because proof >> assistant seems to always choose the earliest theorem, while, for the sake >> of presentation, I might prefer to use a later version that accomplishes >> the same thing. Sometimes I will restate earlier theorems just to group >> them ( for instance, restating all natural deduction rules in one place ). >> >> In any case, this means I sometimes need to clear the justification field >> and carefully type in the name of the theorem I wish to use. This process >> would be faster if there was a feature where instead of using the proof >> assistant I could simply type a search query and pick from a list. >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/577b4292-44bb-4a09-a003-73fa3133fbe1n%40googlegroups.com.
