Expression of type ExprTuple

from the theory of proveit.physics.quantum.QPE

import proveit
# Automation is not needed when building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_expr # Load the stored expression as 'stored_expr'
# import Expression classes needed to build the expression
from proveit import Conditional, ExprTuple, Lambda, m
from proveit.logic import And, InSet
from proveit.physics.quantum.QPE import _m_domain, _phase_est_circuit, _success_cond

# build up the expression from sub-expressions
expr = ExprTuple(Lambda(m, Conditional(_phase_est_circuit, And(InSet(m, _m_domain), _success_cond))))

expr:

# check that the built expression is the same as the stored expression
assert expr == stored_expr
assert expr._style_id == stored_expr._style_id
print("Passed sanity check: expr matches stored_expr")

Passed sanity check: expr matches stored_expr

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\left(m \mapsto \left\{\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert m \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m \rangle_{t}} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \ghost{\textrm{QPE}\left(U, t\right)} & \measure{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} \qw & \ghostqout{\lvert m \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array} \textrm{ if } m \in \{0~\ldotp \ldotp~2^{t} - 1\} ,  \left|\frac{m}{2^{t}} - \varphi\right|_{\textup{mod}\thinspace 1} \leq 2^{-n}\right..\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	ExprTuple	1
1	Lambda	parameter: 114 body: 3
2	ExprTuple	114
3	Conditional	value: 4 condition: 5
4	Operation	operator: 6 operands: 7
5	Operation	operator: 8 operands: 9
6	Literal
7	ExprTuple	10, 11, 12, 13
8	Literal
9	ExprTuple	14, 15
10	ExprTuple	16, 17
11	ExprTuple	18, 19
12	ExprTuple	20, 21
13	ExprTuple	22, 23
14	Operation	operator: 24 operands: 25
15	Operation	operator: 26 operands: 27
16	ExprRange	lambda_map: 28 start_index: 115 end_index: 120
17	ExprRange	lambda_map: 29 start_index: 115 end_index: 116
18	ExprRange	lambda_map: 30 start_index: 115 end_index: 120
19	ExprRange	lambda_map: 30 start_index: 97 end_index: 98
20	ExprRange	lambda_map: 31 start_index: 115 end_index: 120
21	ExprRange	lambda_map: 32 start_index: 115 end_index: 116
22	ExprRange	lambda_map: 33 start_index: 115 end_index: 120
23	ExprRange	lambda_map: 34 start_index: 115 end_index: 116
24	Literal
25	ExprTuple	114, 35
26	Literal
27	ExprTuple	36, 37
28	Lambda	parameter: 96 body: 38
29	Lambda	parameter: 96 body: 39
30	Lambda	parameter: 96 body: 40
31	Lambda	parameter: 96 body: 41
32	Lambda	parameter: 96 body: 42
33	Lambda	parameter: 96 body: 43
34	Lambda	parameter: 96 body: 45
35	Operation	operator: 86 operands: 46
36	Operation	operator: 47 operands: 48
37	Operation	operator: 117 operands: 49
38	Operation	operator: 78 operands: 50
39	Operation	operator: 57 operands: 51
40	Operation	operator: 57 operands: 52
41	Operation	operator: 53 operands: 54
42	Operation	operator: 79 operands: 55
43	Operation	operator: 57 operands: 56
44	ExprTuple	96
45	Operation	operator: 57 operands: 58
46	ExprTuple	59, 60
47	Literal
48	ExprTuple	61, 115
49	ExprTuple	119, 62
50	NamedExprs	state: 63
51	NamedExprs	element: 64 targets: 72
52	NamedExprs	element: 65 targets: 66
53	Literal
54	NamedExprs	basis: 67
55	NamedExprs	operation: 68
56	NamedExprs	element: 69 targets: 70
57	Literal
58	NamedExprs	element: 71 targets: 72
59	Literal
60	Operation	operator: 109 operands: 73
61	Operation	operator: 109 operands: 74
62	Operation	operator: 102 operand: 91
63	Operation	operator: 76 operand: 92
64	Operation	operator: 78 operands: 85
65	Operation	operator: 79 operands: 80
66	Operation	operator: 86 operands: 81
67	Literal
68	Literal
69	Operation	operator: 84 operands: 82
70	Operation	operator: 86 operands: 83
71	Operation	operator: 84 operands: 85
72	Operation	operator: 86 operands: 87
73	ExprTuple	111, 88
74	ExprTuple	89, 90
75	ExprTuple	91
76	Literal
77	ExprTuple	92
78	Literal
79	Literal
80	NamedExprs	operation: 93 part: 96
81	ExprTuple	115, 98
82	NamedExprs	state: 94 part: 96
83	ExprTuple	115, 120
84	Literal
85	NamedExprs	state: 95 part: 96
86	Literal
87	ExprTuple	97, 98
88	Operation	operator: 102 operand: 115
89	Operation	operator: 100 operands: 101
90	Operation	operator: 102 operand: 112
91	Literal
92	Literal
93	Operation	operator: 104 operands: 105
94	Operation	operator: 106 operands: 107
95	Literal
96	Variable
97	Operation	operator: 109 operands: 108
98	Operation	operator: 109 operands: 110
99	ExprTuple	115
100	Literal
101	ExprTuple	114, 111
102	Literal
103	ExprTuple	112
104	Literal
105	ExprTuple	113, 120
106	Literal
107	ExprTuple	114, 120
108	ExprTuple	120, 115
109	Literal
110	ExprTuple	120, 116
111	Operation	operator: 117 operands: 118
112	Literal
113	Literal
114	Variable
115	Literal
116	Literal
117	Literal
118	ExprTuple	119, 120
119	Literal
120	Literal