# ExprTuple¶

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

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. deduce_equality(self, equality, \*[, …]) Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults. 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. Yield the argument values or (name, value) pairs that could be used to recreate the ExprTuple. 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)[source]

Returns true if the entry contains an ExprRange.

deduce_equality(self, equality, \*, eq_via_elem_eq_thm=None, \*\*defaults_config)[source]

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

‘equated’ returns the right-hand side of ‘deduce_equality’. ‘equate’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘deduce_equality’ for the inner expression.

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

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)[source]

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)[source]
is_double(self)[source]

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

is_single(self)[source]

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

latex(self, \*\*kwargs)[source]

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)[source]

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)[source]

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)[source]

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

remake_arguments(self)[source]

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

remake_with_style_calls(self)[source]

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)[source]

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)[source]

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)[source]
with_wrapping_at(self, \*wrap_positions)[source]
wrap_positions(self)[source]

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