search

digama0 / mm0

Metamath Zero specification language
Creative Commons Zero v1.0 Universal
312 stars 40 forks source link

Error handling #125

Open uniwuni opened 1 year ago

uniwuni commented 1 year ago

Is there a way to try multiple tactics on a goal, even if one of them fails? refine errors seem unrecoverable, and there doesn't seem to be any method for comparing goals "up to substitution".

digama0 commented 1 year ago

No, currently all errors are unrecoverable and I am not sure whether it would be a good idea to change that. Maybe a better option would be an explicit snapshot mechanism (to roll back bad unifications) and a try_refine function you could call which returns #undef on substitution failure.

uniwuni commented 1 year ago

Yeah, that seems like the most reasonable solution, and I was honestly a little surprised how far you have come without this feature

digama0 commented 1 year ago

I don't use unification for proof search, and TBH I consider it an anti-pattern. But I'm willing to add it to make it more usable for others.