summaryrefslogtreecommitdiff
path: root/test/examples/calc.tex
diff options
context:
space:
mode:
Diffstat (limited to 'test/examples/calc.tex')
-rw-r--r--test/examples/calc.tex33
1 files changed, 33 insertions, 0 deletions
diff --git a/test/examples/calc.tex b/test/examples/calc.tex
new file mode 100644
index 0000000..b0a0386
--- /dev/null
+++ b/test/examples/calc.tex
@@ -0,0 +1,33 @@
+\begin{proposition}\label{trivial}
+ $x = x$.
+\end{proposition}
+
+\begin{proposition}\label{irrelevant}
+ $z = z$.
+\end{proposition}
+
+\begin{proposition}\label{alsotrivial}
+ $y = y$.
+\end{proposition}
+\begin{proof}
+ \begin{align*}
+ y
+ &= y
+ \\
+ &= y
+ \explanation{by \cref{trivial}}
+ \end{align*}
+\end{proof}
+
+\begin{proposition}\label{trivial_biconditionals}
+ $y = y$.
+\end{proposition}
+\begin{proof}
+ \begin{align*}
+ y = y
+ &\iff \top
+ \\
+ &\iff y = y
+ \explanation{by \cref{trivial}}
+ \end{align*}
+\end{proof}