Skip to content

GitLab

Open
Created by Ralf Jung@jungOwner

Better errors when tactic fails to automatically resolve some side-condition

@robbertkrebbers and me sketched a plan (or rather, two possible plans) for how to show better error messages for common stumbling blocks, such as iMod with mismatching masks:

  1. ElimModal already has support for a pure side-condition; we could introduce something like
Definition pm_error (s : string) := False

and add instances with error "foo" as their side-condition; together with some support in iSolveSideCondition this could be used to then show better, instance-specific error messages when iMod fails.

  1. We could add a new typeclass like ElimModalError that is used to compute an error message when ElimModal failed to find an instance.

Since this is used for diagnostics only, there are no backwards compatibility concerns -- so I feel like we should start with the first approach, since it is easy to implement; we can always switch to something more principled later.

Edited by Ralf Jung