relation_prover

proveit.relation_prover(func)

@relation_prover is a decorator for methods that are to return a proven judgment valid under “active” (default) assumptions, is a Relation type Expression, and has the original expression (self or self.expr) on the left hand side. This “original expression” will automatically be “preserved” (not automatically simplified). The style of the original expression will be used on the left side. As with @prover methods, defaults may be temporarily set.