Skip to content
Snippets Groups Projects
Commit f359b2bc authored by Hans-Jörg's avatar Hans-Jörg
Browse files

Add eq_symmetric to rule classification tables

parent 5ad781d4
No related branches found
No related tags found
No related merge requests found
Pipeline #38138 passed
......@@ -101,6 +101,7 @@ to quickly find the definition of rules.
\ruleref{distinct_elim} & Elimination of the $\lsymb{distinct}$ operator. \\
\ruleref{la_rw_eq} & $(t ≈ u)(t \leq u \land u \leq t)$ \\
\ruleref{nary_elim} & Eliminate $n$-ary application of operators via binary applications. \\
\ruleref{eq_symmetric} & Symmetry of equality as equivalence. \\
\end{xltabular}
\begin{xltabular}{\linewidth}{l X}
......@@ -256,6 +257,14 @@ simplifications.}
\ruleref{symm} & Symmetry of equality. \\
\ruleref{not_symm} & Symmetry of not-equal.\\
\end{xltabular}
\begin{xltabular}{\linewidth}{l X}
\caption{Rules used by the Carcara elaborator.}
\label{rule-tab:cvc5}\\
Rule & Description \\
\hline
\ruleref{eq_symmetric} & Symmetry of equality as equivalence. \\
\end{xltabular}
\subsection{Rule List}
\label{sec:alethe:rules-list}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment