ExprTuple

class proveit.ExprTuple(*expressions, styles=None)

Bases: proveit.Composite, proveit.Expression

An ExprTuple is a composite Expression composed of an ordered list of member Expression “entries”. The ExprTuple represents a mathematical tuple as an ordered collection of “elements”. Each entry may either represent a single element or a “range” of elements. An entry that is an ExprRange represents a range of elements. For example, (a, b, x_1, …, x_n, c, d) Is represented by an ExprTuple with 5 entries representing n+4 elements.

Methods Summary

contains_range(self)	Returns true if the entry contains an ExprRange.
formatted(self, format_type, \*[, fence, …])	Returns a formatted version of the expression for the given format_type (‘string’ or ‘latex’).
has_matching_ranges(self, other_tuple)	Return True iff the other_tuple matches this ExprTuple with respect to which entries are ExprRanges and, where they are, the start and end indices of the ExprRanges match.
index(self, entry[, start, stop])
is_double(self)	Returns True if this has two elements that are not ExprRanges.
is_single(self)	Return True if this has a single element that is not an ExprRange.
latex(self, \*\*kwargs)	Return a latex-formatted representation of the Expression.
merged(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘merger’.
merger(self, \*\*defaults_config)	If this is an tuple of expressions that can be directly merged together into a single ExprRange, return this proven equivalence. For example, {j in Natural, k-(j+1) in Natural} |- (x_1, .., x_j, x_{j+1}, x_{j+2}, …, x_k) = (x_1, …, x_k).
num_elements(self[, proven])	Return the number of elements of this ExprTuple as an Expression.
num_entries(self)	Return the number of entries of the list.
remake_arguments(self)	Yield the argument values or (name, value) pairs that could be used to recreate the ExprTuple.
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 a StyleOptions object that indicates the possible styles and values that is available to determine how this Expression may be presented.
with_justification(self, justification)
with_wrapping_at(self, \*wrap_positions)
wrap_positions(self)	Return a list of wrap positions according to the current style setting.

Methods Documentation

contains_range(self)

Returns true if the entry contains an ExprRange.

formatted(self, format_type, \*, fence=True, sub_fence=False, operator_or_operators=', ', implicit_first_operator=True, wrap_positions=None, justification=None, \*\*kwargs)

Returns a formatted version of the expression for the given format_type (‘string’ or ‘latex’). In the keyword arguments, fence=True indicates that parenthesis around the sub-expression may be necessary to avoid ambiguity.

has_matching_ranges(self, other_tuple)

Return True iff the other_tuple matches this ExprTuple with respect to which entries are ExprRanges and, where they are, the start and end indices of the ExprRanges match.

index(self, entry, start=0, stop=None)

is_double(self)

Returns True if this has two elements that are not ExprRanges.

is_single(self)

Return True if this has a single element that is not an ExprRange.

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).

merged(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘merger’.

merger(self, \*\*defaults_config)

If this is an tuple of expressions that can be directly merged together into a single ExprRange, return this proven equivalence. For example, {j in Natural, k-(j+1) in Natural} |- (x_1, .., x_j, x_{j+1}, x_{j+2}, …, x_k) = (x_1, …, x_k)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘merged’ returns the right-hand side of ‘merger’. ‘merge’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘merger’ for the inner expression.

num_elements(self, proven=True, \*\*defaults_config)

Return the number of elements of this ExprTuple as an Expression. This includes the extent of all contained ranges. If proven==True, a proof is constructed in the process.

num_entries(self)

Return the number of entries of the list. Some entries may be ranges (ExprRange) that represent multiple elements of the list.

remake_arguments(self)

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

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 a StyleOptions object that indicates the possible styles and values that is available to determine how this Expression may be presented.

with_justification(self, justification)

with_wrapping_at(self, \*wrap_positions)

wrap_positions(self)

Return a list of wrap positions according to the current style setting. Position ‘n’ is after the nth comma.