Operation

class proveit.Operation(operator, operand_or_operands=None, *, operands=None, styles)

Bases: proveit.Expression

Attributes Summary

operation_class_of_operator

Methods Summary

extract_init_arg_value(arg_name, operator, …)	Given a name of one of the arguments of the __init__ method, return the corresponding value contained in the ‘operands’ composite expression (i.e., the operands of a constructed operation).
extract_my_init_arg_value(self, arg_name)	Given a name of one of the arguments of the __init__ method, return the corresponding value appropriate for reconstructing self.
latex(self, \*\*kwargs)	Return a latex-formatted representation of the Expression.
remake_arguments(self)	Yield the argument values or (name, value) pairs that could be used to recreate the Operation.
remake_with_style_calls(self)	In order to reconstruct this Expression to have the same styles, what “with…” method calls are most appropriate? Return a tuple of strings with the calls to make.
string(self, \*\*kwargs)	Return a string representation of the Expression.
style_options(self)	Return the StyleOptions object for the Operation.
with_justification(self, justification)
with_wrap_after_operator(self)
with_wrap_before_operator(self)
with_wrapping_at(self, \*wrap_positions)
wrap_positions(self)	Return a list of wrap positions according to the current style setting.

Attributes Documentation

operation_class_of_operator = {o: <class 'proveit._core_.expression.lambda_expr.composition.Composition'>, CondSet: <class 'proveit._core_.expression.conditional.conditional_set.ConditionalSet'>, length: <class 'proveit.core_expr_types.tuples.length.Len'>, Interval: <class 'proveit.numbers.number_sets.integers.interval.Interval'>, forall: <class 'proveit.logic.booleans.quantification.universality.forall.Forall'>, exists: <class 'proveit.logic.booleans.quantification.existence.exists.Exists'>, notexists: <class 'proveit.logic.booleans.quantification.existence.not_exists.NotExists'>, exists!: <class 'proveit.logic.booleans.quantification.existence.unique_exists.UniqueExists'>, in_c: <class 'proveit.logic.classes.membership.in_class.InClass'>, not-in_{C}: <class 'proveit.logic.classes.membership.not_in_class.NotInClass'>, in: <class 'proveit.logic.sets.membership.in_set.InSet'>, not-in: <class 'proveit.logic.sets.membership.not_in_set.NotInSet'>, Groups: <class 'proveit.abstract_algebra.groups.groups.Groups'>, Rings: <class 'proveit.abstract_algebra.rings.rings.Rings'>, Fields: <class 'proveit.abstract_algebra.fields.fields.Fields'>, Set: <class 'proveit.logic.sets.enumeration.enum_set.Set'>, subset_eq: <class 'proveit.logic.sets.inclusion.subset_eq.SubsetEq'>, not_subset_eq: <class 'proveit.logic.sets.inclusion.not_subset_eq.NotSubsetEq'>, proper_subset: <class 'proveit.logic.sets.inclusion.proper_subset.ProperSubset'>, not_proper_subset: <class 'proveit.logic.sets.inclusion.not_proper_subset.NotProperSubset'>, equiv: <class 'proveit.logic.sets.equivalence.set_equiv.SetEquiv'>, not_equiv: <class 'proveit.logic.sets.equivalence.set_not_equiv.SetNotEquiv'>, union: <class 'proveit.logic.sets.unification.union.Union'>, union_of_all: <class 'proveit.logic.sets.unification.union_all.UnionAll'>, intersect: <class 'proveit.logic.sets.intersection.intersect.Intersect'>, intersect_all: <class 'proveit.logic.sets.intersection.intersect_all.IntersectAll'>, -: <class 'proveit.logic.sets.subtraction.difference.Difference'>, SetOfAll: <class 'proveit.logic.sets.comprehension.set_of_all.SetOfAll'>, power_set: <class 'proveit.logic.sets.power_set.power_set.PowerSet'>, CartExp: <class 'proveit.logic.sets.cartesian_products.cart_exp.CartExp'>, X: <class 'proveit.logic.sets.cartesian_products.cart_prod.CartProd'>, disjoint: <class 'proveit.logic.sets.disjointness.disjoint.Disjoint'>, distinct: <class 'proveit.logic.sets.disjointness.distinct.Distinct'>, card: <class 'proveit.logic.sets.cardinality.cardinality.Card'>, Functions: <class 'proveit.logic.sets.functions.functions.Functions'>, IMAGE: <class 'proveit.logic.sets.functions.images.image.Image'>, INV_IMAGE: <class 'proveit.logic.sets.functions.images.inverse_image.InvImage'>, Injections: <class 'proveit.logic.sets.functions.injections.injections.Injections'>, Surjections: <class 'proveit.logic.sets.functions.surjections.surjections.Surjections'>, Bijections: <class 'proveit.logic.sets.functions.bijections.bijections.Bijections'>, =: <class 'proveit.logic.equality.equals.Equals'>, !=: <class 'proveit.logic.equality.not_equals.NotEquals'>, and: <class 'proveit.logic.booleans.conjunction.and_op.And'>, or: <class 'proveit.logic.booleans.disjunction.or_op.Or'>, not: <class 'proveit.logic.booleans.negation.not_op.Not'>, =>: <class 'proveit.logic.booleans.implication.implies.Implies'>, <=>: <class 'proveit.logic.booleans.implication.iff.Iff'>, Decimal: <class 'proveit.numbers.numerals.decimals.deci.DecimalSequence'>, Binary: <class 'proveit.numbers.numerals.binaries.binary_sequence.BinarySequence'>, IntervalOO: <class 'proveit.numbers.number_sets.real_numbers.interval.IntervalOO'>, IntervalOC: <class 'proveit.numbers.number_sets.real_numbers.interval.IntervalOC'>, IntervalCO: <class 'proveit.numbers.number_sets.real_numbers.interval.IntervalCO'>, IntervalCC: <class 'proveit.numbers.number_sets.real_numbers.interval.IntervalCC'>, conj: <class 'proveit.numbers.number_sets.complex_numbers.conjugate.Conjugate'>, round: <class 'proveit.numbers.rounding.round.Round'>, ceil: <class 'proveit.numbers.rounding.ceil.Ceil'>, floor: <class 'proveit.numbers.rounding.floor.Floor'>, Abs: <class 'proveit.numbers.absolute_value.abs.Abs'>, +: <class 'proveit.numbers.addition.add.Add'>, -: <class 'proveit.numbers.negation.neg.Neg'>, <: <class 'proveit.numbers.ordering.less.Less'>, <=: <class 'proveit.numbers.ordering.less_eq.LessEq'>, Max: <class 'proveit.numbers.ordering.max.Max'>, Min: <class 'proveit.numbers.ordering.min.Min'>, *: <class 'proveit.numbers.multiplication.mult.Mult'>, /: <class 'proveit.numbers.division.divide.Div'>, |: <class 'proveit.numbers.divisibility.divides.Divides'>, |: <class 'proveit.numbers.divisibility.divides.DividesProper'>, gcd: <class 'proveit.numbers.divisibility.greatest_common_divisor.GCD'>, mod: <class 'proveit.numbers.modular.mod.Mod'>, ModAbs: <class 'proveit.numbers.modular.mod_abs.ModAbs'>, Exp: <class 'proveit.numbers.exponentiation.exp.Exp'>, log: <class 'proveit.numbers.logarithms.log.Log'>, Sum: <class 'proveit.numbers.summation.sum.Sum'>, Prod: <class 'proveit.numbers.product.prod.Prod'>, Integrate: <class 'proveit.numbers.integration.integrate.Integrate'>, MonDecFuncs: <class 'proveit.numbers.functions.mon_dec_funcs.MonDecFuncs'>, Kdelta: <class 'proveit.numbers.functions.delta.KroneckerDelta'>}

Methods Documentation

classmethod extract_init_arg_value(arg_name, operator, operands)

Given a name of one of the arguments of the __init__ method, return the corresponding value contained in the ‘operands’ composite expression (i.e., the operands of a constructed operation).

Except when this is an OperationOverInstances, this method should be overridden if you cannot simply pass the operands directly into the __init__ method.

extract_my_init_arg_value(self, arg_name)

Given a name of one of the arguments of the __init__ method, return the corresponding value appropriate for reconstructing self. The default calls the extract_init_arg_value static method. Overload this when the most proper way to construct the expression is style dependent. Then “remake_arguments” will use this overloaded method. “_make” will do it via the static method but will fix the styles afterwards.

latex(self, \*\*kwargs)

Return a latex-formatted representation of the Expression. The kwargs can contain formatting directives (such as ‘fence’ used to indicate when a sub-expression should be wrapped in parentheses if there can be ambiguity in the order of operations).

remake_arguments(self)

Yield the argument values or (name, value) pairs that could be used to recreate the Operation.

remake_with_style_calls(self)

In order to reconstruct this Expression to have the same styles, what “with…” method calls are most appropriate? Return a tuple of strings with the calls to make. The default for the Operation class is to include appropriate ‘with_wrapping_at’ and ‘with_justification’ calls.

string(self, \*\*kwargs)

Return a string representation of the Expression. The kwargs can contain formatting directives (such as ‘fence’ used to indicate when a sub-expression should be wrapped in parentheses if there can be ambiguity in the order of operations).

style_options(self)

Return the StyleOptions object for the Operation.

with_justification(self, justification)

with_wrap_after_operator(self)

with_wrap_before_operator(self)

with_wrapping_at(self, \*wrap_positions)

wrap_positions(self)

Return a list of wrap positions according to the current style setting.