logo

Theory of proveit.core_expr_types

Theory related to Expression types defined in Prove-It's core.

In [1]:
import proveit
%theory # toggles between interactive and static modes

Local content of this theory

common expressions axioms theorems demonstrations

Sub-theories

operationstheory pertaining to Operation expressions
conditionalstheory pertaining to Conditional expressions
lambda_mapstheory pertaining to Lambda expressions
tuplestheory pertaining to ExprTuple and ExprRange types
indexed_varstheory pertaining to IndexedVar types
expr_arraysAn ExprArray is an ExprTuple of ExprTuples presented in a 2-D format

All axioms contained within this theory

This theory contains no axioms directly.

proveit.core_expr_types.operations

proveit.core_expr_types.operations.operands_substitution

proveit.core_expr_types.conditionals

proveit.core_expr_types.conditionals.true_condition_reduction
proveit.core_expr_types.conditionals.condition_replacement
proveit.core_expr_types.conditionals.condition__as__condition_eq_true
proveit.core_expr_types.conditionals.conditional_substitution
proveit.core_expr_types.conditionals.true_case_reduction

proveit.core_expr_types.lambda_maps

proveit.core_expr_types.lambda_maps.lambda_substitution
proveit.core_expr_types.lambda_maps.unary_composition
proveit.core_expr_types.lambda_maps.binary_composition
proveit.core_expr_types.lambda_maps.multi_composition_def

proveit.core_expr_types.tuples

proveit.core_expr_types.tuples.tuple_len_0
proveit.core_expr_types.tuples.tuple_len_incr
proveit.core_expr_types.tuples.tuple_eq_def
proveit.core_expr_types.tuples.tuple_neq_with_diff_len
proveit.core_expr_types.tuples.empty_range_def
proveit.core_expr_types.tuples.range_extension_def

proveit.core_expr_types.indexed_vars

This sub-theory contains no axioms.

proveit.core_expr_types.expr_arrays

proveit.core_expr_types.expr_arrays.array_eq_def
proveit.core_expr_types.expr_arrays.varray_eq_def
proveit.core_expr_types.expr_arrays.array_neq_with_diff_len
proveit.core_expr_types.expr_arrays.varray_neq_with_diff_len