> Can you describe one or few such cases when lamp doesn't behave as you expect? I will try to find an explanation to lamp’s behavior, and check if it is not a bug.
Usually lamp wouldn't be able to figure out some step which uses a theorem from christmas25.mm. Once I do that step manually, it is able to fill in the rest of the proof (of course I tried switching the "Less" and "LessEq" settings to "unrestricted"). Now in hindsight I think that I should have saved a couple of proofs like that to serve as an example for you :-( I'll make sure to open an issue if I stumble upon such a proof again. -- 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 visit https://groups.google.com/d/msgid/metamath/acfb89b6-66bc-46ee-b943-d21471251dbfn%40googlegroups.com.
