Open sankalpgambhir opened 1 year ago
Probably a bigger issue, is that these are not caught during proof construction to return an InvalidProofTactic
, but rather throw (currently uncaught) exceptions.
Yep. Same issue is application of functions with incorrect number of parameters. Not sure yet about the best solution, but probably involves constructors from outside the kernel. That's in my mind :D
Failed
require
s currently give rather unhelpful errors. Eg:is improper, since
Z
has arity 1 whileh
, 2. However, this simply returns the error:We could probably stand to improve these errors for easier proof debugging.