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 ExprTuple
from proveit.physics.quantum.QPE import _phase_est_circuit

# build up the expression from sub-expressions
expr = ExprTuple(_phase_est_circuit)

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(\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}\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	Operation	operator: 2 operands: 3
2	Literal
3	ExprTuple	4, 5, 6, 7
4	ExprTuple	8, 9
5	ExprTuple	10, 11
6	ExprTuple	12, 13
7	ExprTuple	14, 15
8	ExprRange	lambda_map: 16 start_index: 78 end_index: 79
9	ExprRange	lambda_map: 17 start_index: 78 end_index: 80
10	ExprRange	lambda_map: 18 start_index: 78 end_index: 79
11	ExprRange	lambda_map: 18 start_index: 67 end_index: 68
12	ExprRange	lambda_map: 19 start_index: 78 end_index: 79
13	ExprRange	lambda_map: 20 start_index: 78 end_index: 80
14	ExprRange	lambda_map: 21 start_index: 78 end_index: 79
15	ExprRange	lambda_map: 22 start_index: 78 end_index: 80
16	Lambda	parameter: 66 body: 23
17	Lambda	parameter: 66 body: 24
18	Lambda	parameter: 66 body: 25
19	Lambda	parameter: 66 body: 26
20	Lambda	parameter: 66 body: 27
21	Lambda	parameter: 66 body: 28
22	Lambda	parameter: 66 body: 30
23	Operation	operator: 52 operands: 31
24	Operation	operator: 38 operands: 32
25	Operation	operator: 38 operands: 33
26	Operation	operator: 34 operands: 35
27	Operation	operator: 53 operands: 36
28	Operation	operator: 38 operands: 37
29	ExprTuple	66
30	Operation	operator: 38 operands: 39
31	NamedExprs	state: 40
32	NamedExprs	element: 41 targets: 49
33	NamedExprs	element: 42 targets: 43
34	Literal
35	NamedExprs	basis: 44
36	NamedExprs	operation: 45
37	NamedExprs	element: 46 targets: 47
38	Literal
39	NamedExprs	element: 48 targets: 49
40	Operation	operator: 50 operand: 62
41	Operation	operator: 52 operands: 59
42	Operation	operator: 53 operands: 54
43	Operation	operator: 60 operands: 55
44	Literal
45	Literal
46	Operation	operator: 58 operands: 56
47	Operation	operator: 60 operands: 57
48	Operation	operator: 58 operands: 59
49	Operation	operator: 60 operands: 61
50	Literal
51	ExprTuple	62
52	Literal
53	Literal
54	NamedExprs	operation: 63 part: 66
55	ExprTuple	78, 68
56	NamedExprs	state: 64 part: 66
57	ExprTuple	78, 79
58	Literal
59	NamedExprs	state: 65 part: 66
60	Literal
61	ExprTuple	67, 68
62	Literal
63	Operation	operator: 69 operands: 70
64	Operation	operator: 71 operands: 72
65	Literal
66	Variable
67	Operation	operator: 74 operands: 73
68	Operation	operator: 74 operands: 75
69	Literal
70	ExprTuple	76, 79
71	Literal
72	ExprTuple	77, 79
73	ExprTuple	79, 78
74	Literal
75	ExprTuple	79, 80
76	Literal
77	Variable
78	Literal
79	Literal
80	Literal