Instantiation

class proveit.Instantiation(orig_judgment, num_forall_eliminations, repl_map, equiv_alt_expansions, mapping, mapping_key_order, simplify_only_where_marked, markers_and_marked_expr, *, _proven_truth=None, _requirements=None, _marked_req_indices=None)

Bases: proveit.Proof

An Instantiation proof step eliminates some number of nested Forall operations and simultaneously replaces Variables with Expressions according to the replacement map (repl_map). A Variable that is a parameter variable of an internal Lambda expression may only be relabeled; it will not be replaced with a non-Variable expression within the scope of the Lambda expression.

See Expression.substituted for details regarding the replacement rules.

Methods Summary

step_type(self)

Methods Documentation

step_type(self)