From f359b2bc1d7f19ea11029805bf2dc62a1cbbcb32 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Mon, 15 Jul 2024 15:29:23 -0500
Subject: [PATCH] Add eq_symmetric to rule classification tables

---
 spec/rule_list.tex | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 257f36a..4b89550 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -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}
 
-- 
GitLab