Replicating proof checking at the level of construction of DoubleStep based proofs.
the checks for fully parametrized versions of steps replicate checks from SCProofChecker
where possible, unparameterized versions defer checking by calling the parametrized versions, to centralize checking for a given proof step
error messages have been uniformized in tone and speech patterns where spotted. I have opted for active instead of passive tones wherever applicable, "x is not y" instead of "x must be y". Previously, both existed simultaneously.
a requirement during checking was to make sure the correct number of premises has been provided to the step. A suggestion offered was to make the step a function of arity N where N is a type parameter provided as ProofStepWithoutBotNorPrem[N]. I have not found a way to do this in Scala yet, outside of adding a require statement to the function, which in my opinion, produces a relatively unhelpful error message with respect to tracking it down. Currently, I have implemented them as part of the proof checking, and an error is raised in the same manner as a malformed proof step:
However, in the short term, this will make error reporting worse till #85 is resolved, since all the errors are expected to be reported through the tactic system. DO NOT MERGE before it is resolved or the status is accordingly updated above.
