ExprRange

class proveit.ExprRange(parameter, body, start_index=None, end_index=None, *, true_start_index=None, true_end_index=None, use_canonical_parameter=True, parameterization=None, lambda_map=None, order=None, styles=None)

Bases: proveit.Expression

An ExprRange expression represents a range of “element” expressions within a containing ExprTuple. It represents this as a Lambda to map each valid index value to a corresponding element, along with a start and end index value. The represented element sequence corresponds to index values going from the start to the end in increments of 1, ranging over index values.

For example, 1/i + … + 1/j is internall represented by an Add operation with the following as its “operands”: (1/i, …, 1/j). These “operands” are represented by an ExprTuple with a single “entry” which is an ExprRange whose lambda_map is “k |-> 1/k”, start_index is “i”, and end_index is “j”. An ExprTuple “entry” may generally either be a singuler element or an ExprRange that represents multiple elements.

Methods Summary

end_indices(self)	Return a list of ending indices, one for each nested ExprRange. For example, (x_{m, i_{m}}, …, x_{m, j_{m}}, ……, x_{n, i_{n}}, …, x_{n, j_{n}}). has end indices (n, j_n).
first(self)	Return the first instance of the range.
formatted(self, format_type, \*\*kwargs)	Returns a formatted version of the expression for the given format_type (‘string’ or ‘latex’).
innermost_body(self)	Return the innermost body of a nested ExprRange.
last(self)	Return the last instance of the range.
latex(self, \*\*kwargs)	Return a latex-formatted representation of the Expression.
literal_int_extent(self)	If the start and end indices of this ExprRange are literal integers, return the literal number of elements of the ExprRange. For the case of nested ExprRange’s, all of the start and end indices must be integers and the result will be the multiplied extent. For example: a_{1,1}, …, a_{1,3}, ……, a_{4,1}, …, a_{4,3} has a literal_int_extent of 12.
mapped_range(self, body_map_fn)	Generate an ExprRange with the same external structure as this range but converts the innermost by applying the ‘body_map_fn’ to it.
nested_range_depth(self)	Return the depth of nested ranges.
parameters(self)	Return a list of parameters, one for each nested ExprRange.
partition(self, before_split_idx, \*[, …])	Return the equation between this range within an ExprTuple and a split version in the following manner: (f(self.true_start_index), …, f(self.true_end_index)) = (f(self.true_start_index), …, f(before_split_index), f(before_split_index+1), …, f(self.true_end_index)) where f represents the self.lambda_map.
partitioned(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘partition’.
remake_arguments(self)	Yield the argument values or (name, value) pairs that could be used to recreate the ExprRange.
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.
shift_equivalence(self, \*[, old_shift, …])	Return the equation between this range within an ExprTuple and a shifted version in the following manner: (f(self.true_start_index+old_shift), …, f(self.true_end_index+old_shift)) = (f(new_start+new_shift), …, f(new_start+new_shift)) where f is adapted from self.lambda_map according to ‘old_shift’. If any of the ‘new’ parameters are unspecified, we attempt to deduce them from the other parameters.
start_indices(self)	Return a list of starting indices, one for each nested ExprRange. For example, (x_{m, i_{m}}, …, x_{m, j_{m}}, ……, x_{n, i_{n}}, …, x_{n, j_{n}}). has start indices (m, i_m).
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_default_parameterization_style(self)	The default is to use an ‘implicit’ parameterization for string formatting (see ‘with_implicit_parameterization’) and and ‘explicit’ parameterization for LaTeX formatting (see ‘with_explicit_parameterization’).
with_explicit_parameterization(self)	The ‘parameterization’:’explicit’ style shows the parameterization of the ExprRange explicitly.
with_implicit_parameterization(self)	The ‘parameterization’:’implicit’ style does not show the parameterization of the ExprRange explicitly and such that the parameterization may be ambiguous but is more compact.

Methods Documentation

end_indices(self)

Return a list of ending indices, one for each nested ExprRange. For example,

(x_{m, i_{m}}, …, x_{m, j_{m}}, ……,

x_{n, i_{n}}, …, x_{n, j_{n}}).

has end indices (n, j_n).

first(self)

Return the first instance of the range.

formatted(self, format_type, \*\*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.

innermost_body(self)

Return the innermost body of a nested ExprRange.

last(self)

Return the last instance of the range.

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

literal_int_extent(self)

If the start and end indices of this ExprRange are literal integers, return the literal number of elements of the ExprRange. For the case of nested ExprRange’s, all of the start and end indices must be integers and the result will be the multiplied extent. For example:

a_{1,1}, …, a_{1,3}, ……, a_{4,1}, …, a_{4,3}

has a literal_int_extent of 12.

mapped_range(self, body_map_fn)

Generate an ExprRange with the same external structure as this range but converts the innermost by applying the ‘body_map_fn’ to it.

nested_range_depth(self)

Return the depth of nested ranges. For example, if this is a simple range with no nesting, return 1. If this is a range of simple ranges, return 2. If this is a range of ranges of simple ranges, return 3.

parameters(self)

Return a list of parameters, one for each nested ExprRange.

partition(self, before_split_idx, \*, force_to_treat_as_increasing=False, \*\*defaults_config)

Return the equation between this range within an ExprTuple and a split version in the following manner:

(f(self.true_start_index), …, f(self.true_end_index)) = (f(self.true_start_index), …, f(before_split_index),

f(before_split_index+1), …, f(self.true_end_index))

where f represents the self.lambda_map.

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

‘partitioned’ returns the right-hand side of ‘partition’. ‘split’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘partition’ for the inner expression.

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

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

remake_arguments(self)

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

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.

shift_equivalence(self, \*, old_shift=None, new_start=None, new_end=None, new_shift=None, force_to_treat_as_increasing=False, \*\*defaults_config)

Return the equation between this range within an ExprTuple and a shifted version in the following manner:

(f(self.true_start_index+old_shift), …, f(self.true_end_index+old_shift)) = (f(new_start+new_shift), …, f(new_start+new_shift))

where f is adapted from self.lambda_map according to ‘old_shift’. If any of the ‘new’ parameters are unspecified, we attempt to deduce them from the other parameters.

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

‘shifted’ returns the right-hand side of ‘shift_equivalence’. ‘shift’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘shift_equivalence’ for the inner expression.

start_indices(self)

Return a list of starting indices, one for each nested ExprRange. For example,

(x_{m, i_{m}}, …, x_{m, j_{m}}, ……,

x_{n, i_{n}}, …, x_{n, j_{n}}).

has start indices (m, i_m).

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_default_parameterization_style(self)

The default is to use an ‘implicit’ parameterization for string formatting (see ‘with_implicit_parameterization’) and and ‘explicit’ parameterization for LaTeX formatting (see ‘with_explicit_parameterization’).

with_explicit_parameterization(self)

The ‘parameterization’:’explicit’ style shows the parameterization of the ExprRange explicitly. For example, x_{1+1}, ..x_{k+1}.., x_{n+1}).

with_implicit_parameterization(self)

The ‘parameterization’:’implicit’ style does not show the parameterization of the ExprRange explicitly and such that the parameterization may be ambiguous but is more compact. For example, x_{1+1}, …, x_{n+1} could be x_{1+1}, ..x_{k+1}.., x_{n+1} or could be x_{1+1}, ..x_{k}.., x_{n+1}.