equality_prover

proveit.equality_prover(past_tense, present_tense, automatic=False)

@equality_prover works the same way as the @relation_prover decorator except that it also registers the “equality method” in InnerExpr with the past tense and present tense names. The method name itself should be a noun form and return the proven equality with ‘self’ of the method on the left-hand side. Calling the past-tense version will return the right-hand side as equal to ‘self’. The present-tense version can be called on an InnerExpr of a Judgment to return a Judgment where inner expression is replaced according to the equality.