OperationOverInstances

class proveit.OperationOverInstances(operator, instance_param_or_params, instance_expr, *, domain=None, domains=None, condition=None, conditions=None, styles=None, _lambda_map=None)

Bases: proveit.Operation

OperationOverInstances description: TODO

Methods Summary

all_conditions(self)	Returns all conditions of this OperationOverInstances and all conditions of nested OperationOverInstances of the same type.
all_domains(self)	Returns all domains of this OperationOverInstances including domains of nested OperationOverInstances of the same type.
all_instance_params(self)	Returns all instance parameters (each a Variable or Iter of IndexedVars) of this OperationOverInstances and all instance parameters of nested OperationOverInstances.
all_instance_vars(self)	Returns all instance parameter variables of this OperationOverInstances and all instance parameters variables of nested OperationOverInstances.
domain_conditions(self)	Return the domain conditions of all instance variables that are joined together at this level according to the style.
effective_condition(self)	Return the effective ‘condition’ of the OperationOverInstances.
explicit_conditions(self)	Return the conditions that are to be shown explicitly in the formatting (after the “such that” symbol “|”) at this level according to the style.
explicit_domains(self)	Return the domains of the instance variables as a tuple.
explicit_instance_params(self)	Return the instance parameters that are to be shown explicitly in the formatting (as opposed to being made implicit via conditions) joined together at this level according to the style.
explicit_instance_vars(self)	Return the instance parameter variables that are to be shown explicitly in the formatting (as opposed to being made implicit via conditions) joined together at this level according to the style.
extract_my_init_arg_value(self, arg_name)	Return the most proper initialization value for the initialization argument of the given name in order to reconstruct this Expression in its current style.
first_domain(self)
has_domain(self)
has_one_domain(self)	Return True if and only if each instance parameter has the some explicit domain.
instance_param_lists(self)	Returns lists of instance parameters that include all of the instance parameters (see all_instance_params method) but grouped together according to the style joining instance parameters together.
latex(self, \*\*kwargs)	Return a latex-formatted representation of the Expression.
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_wrapping(self[, wrap])	Wraps the ‘instance_expr’ onto the next line. For example
wrap_params(self[, wrap])	Wraps the parameters onto the multiple lines depending on

Methods Documentation

all_conditions(self)

Returns all conditions of this OperationOverInstances and all conditions of nested OperationOverInstances of the same type. Relies on the Python generator function _all_conditions() defined above. Added by wdc on 6/06/2019.

all_domains(self)

Returns all domains of this OperationOverInstances including domains of nested OperationOverInstances of the same type.

all_instance_params(self)

Returns all instance parameters (each a Variable or Iter of IndexedVars) of this OperationOverInstances and all instance parameters of nested OperationOverInstances.

all_instance_vars(self)

Returns all instance parameter variables of this OperationOverInstances and all instance parameters variables of nested OperationOverInstances.

domain_conditions(self)

Return the domain conditions of all instance variables that are joined together at this level according to the style.

effective_condition(self)

Return the effective ‘condition’ of the OperationOverInstances. If there is no ‘condition’, return And operating on zero operands.

explicit_conditions(self)

Return the conditions that are to be shown explicitly in the formatting (after the “such that” symbol “|”) at this level according to the style. By default, this includes all of the ‘joined’ conditions except implicit ‘domain’ conditions.

explicit_domains(self)

Return the domains of the instance variables as a tuple.

explicit_instance_params(self)

Return the instance parameters that are to be shown explicitly in the formatting (as opposed to being made implicit via conditions) joined together at this level according to the style. By default, this includes all of the instance parameters that are to be joined but this may be overridden to exclude implicit instance parameters.

explicit_instance_vars(self)

Return the instance parameter variables that are to be shown explicitly in the formatting (as opposed to being made implicit via conditions) joined together at this level according to the style. The behavior is determined by ‘explicit_instance_params’. Here, we simply extract the variables from the parameters that result from ‘explicit_instance_params’.

extract_my_init_arg_value(self, arg_name)

Return the most proper initialization value for the initialization argument of the given name in order to reconstruct this Expression in its current style.

first_domain(self)

has_domain(self)

has_one_domain(self)

Return True if and only if each instance parameter has the some explicit domain.

instance_param_lists(self)

Returns lists of instance parameters that include all of the instance parameters (see all_instance_params method) but grouped together according to the style joining instance parameters together.

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_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 OperationOverInstances class is to include appropriate ‘with_wrapping’, ‘wrap_params’, 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_wrapping(self, wrap=True)

Wraps the ‘instance_expr’ onto the next line. For example

orall_{a, b, c, d, e, f, g}

P(a, b, c, d, e, f, g)

rather than

orall_{a, b, c, d, e, f, g} P(a, b, c, d, e, f, g)

wrap_params(self, wrap=True)

Wraps the parameters onto the multiple lines depending on how many parameters there are. For example:

orall_{a, b, c,

d, e, f, g} P(a, b, c, d, e, f, g)

rather than

orall_{a, b, c, d, e, f, g} P(a, b, c, d, e, f, g)