Re: [isabelle] Methods with informative failure messages
you could return Seq.empty and print a warning or tracing message.
However, note that in combination with tacticals (like ?,*), your
method might fail multiple times on different goals and produce a whole
bunch of warning messages ... many of them might be useless, but I
don't think there is a general rule to filter the actual informative
On Fr, 2018-05-25 at 11:32 -0400, Dominique Unruh wrote:
> I would like to implement a method that gives an informative error
> when application fails (e.g., imagine an algebra tactic returning
> should not contain <=" or something like that).
> I see possibilities how a method can indicate a failure:
> - Raise an exception
> - Return a (Seq.Error (K "error message")) result.
> - Return Seq.empty (this is what is done by most methods)
> According to my experiments, the first two options are not suitable
> they break method combinators like "method+" and "method?" (I would
> that these will suppress the error.) And the third option does not
> giving an error message.
> Is there any best practice how to return informative messages on
> I feel that this would be very helpful for the user of the method
> often one has to do a lot of try and error to find out why a method
> work on a given subgoal.
> Best wishes,
This archive was generated by a fusion of
Pipermail (Mailman edition) and