From 3038ab9c9624e3ada158b3c0f121e759f794b271 Mon Sep 17 00:00:00 2001
From: Arsh Malik <51771221+ArshMalik02@users.noreply.github.com>
Date: Tue, 4 Jun 2024 13:15:05 -0700
Subject: [PATCH] make descriptions more specific

---
 README.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index 81ba1ab..95724de 100644
--- a/README.md
+++ b/README.md
@@ -38,6 +38,6 @@ proving parts of the appendix or main body of the paper:
 - PartialTraceDefinitions - Adding the functions for tracing out qubits, and
   properties of the function.
 - TraceoutHelpers - Contains helper lemmas for tracing out qubits.
-- DiagonalHelpers.v - Helper lemmas for diagonal matrices.
-- WFHelpers.v - Helper lemmas for well-formed matrices.
-- Permutations.v - Helper lemmas for permutations.
+- DiagonalHelpers.v - Contains helpers lemmas that verify commutativity properties of diagonal matrices and diagonal properties control U and ccu U, where U is a diagonal matrix.
+- WFHelpers.v - Contains the solve_WF_matrix automation tactic for solving well-formedness goals.
+- Permutations.v - Helper lemmas for handling permutations, particularly useful in validating eigenvalue rearrangements and matrix decompositions.