mm0 icon indicating copy to clipboard operation
mm0 copied to clipboard
verified publisher icon digama0

Error handling

Open uniwuni opened this issue 2 years ago • 3 comments

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".

uniwuni avatar May 13 '23 19:05 uniwuni

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.

digama0 avatar May 13 '23 19:05 digama0

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

uniwuni avatar May 13 '23 20:05 uniwuni

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.

digama0 avatar May 13 '23 20:05 digama0