Merge branch 'main' of https://github.com/teorth/equational_theories

amirlb · Sep 28, 2024 · 3474708 · 3474708
2 parents 9b50ada + 8e813bc
commit 3474708
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 1 deletion.
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
@@ -68,6 +68,7 @@ Proofs generated programmatically are also welcome. If you do this, you are enco
 - Then add a single Lean file (e.g., "equational_theories/Generated/MyTechnique.lean") that references all your theorems.
 - Add a README (e.g., "equational_theories/Generated/MyTechnique/README.md") to document how to reproduce your automatically generated theorems (to the extent possible, for randomized algorithms).
 - In [.gitattributes](.gitattributes) add `equational_theories/Generated/MyTechnique.lean linguist-generated` for all automatically generated files.
+- In the file `equational_theories/Generated.lean` add the import line `import equational_theories.Generated.MyTechnique` replacing "MyTechnique" with the name of your folder.
 - Consider adding to the blueprint to explain the automated proof technique used.
 
 ## Images

diff --git a/equational_theories.lean b/equational_theories.lean
@@ -1,3 +1,3 @@
 import equational_theories.Subgraph
 import equational_theories.AllEquations
-import equational_theories.Generated.SimpleRewrites
+import equational_theories.Generated
diff --git a/equational_theories/Generated.lean b/equational_theories/Generated.lean
@@ -0,0 +1,3 @@
+import equational_theories.Generated.SimpleRewrites
+import equational_theories.Generated.Constant
+import equational_theories.Generated.Singleton