From c249ef5670b2c83ec0bfe3e7399ad3b3c4519eff Mon Sep 17 00:00:00 2001
From: Markus Hauru <mhauru@turing.ac.uk>
Date: Fri, 18 Oct 2024 14:31:22 +0100
Subject: [PATCH 1/3] Fix broken export

---
 src/HerbSpecification.jl | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/HerbSpecification.jl b/src/HerbSpecification.jl
index b44ea7b..f3f7c49 100644
--- a/src/HerbSpecification.jl
+++ b/src/HerbSpecification.jl
@@ -15,7 +15,7 @@ export
     Trace,
 
     AbstractTypeSpecification,
-    DependentTypeSpecification,
+    AbstractDependentTypeSpecification,
     AgdaSpecification
 
 end # module HerbSpecification

From 3616c874ef3834fc5fec3cbb7d3e8c2002603ff5 Mon Sep 17 00:00:00 2001
From: Reuben Gardos Reid <5456207+ReubenJ@users.noreply.github.com>
Date: Wed, 23 Oct 2024 13:26:48 +0200
Subject: [PATCH 2/3] Switch to separate test `Project.toml` structure

---
 Project.toml      | 6 ------
 test/Project.toml | 3 +++
 2 files changed, 3 insertions(+), 6 deletions(-)
 create mode 100644 test/Project.toml

diff --git a/Project.toml b/Project.toml
index da70479..f01371d 100644
--- a/Project.toml
+++ b/Project.toml
@@ -7,9 +7,3 @@ version = "0.1.0"
 
 [compat]
 julia = "1.8"
-
-[extras]
-Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
-
-[targets]
-test = ["Test"]
diff --git a/test/Project.toml b/test/Project.toml
new file mode 100644
index 0000000..b35b5ed
--- /dev/null
+++ b/test/Project.toml
@@ -0,0 +1,3 @@
+[deps]
+Aqua = "4c88cf16-eb10-579e-8560-4a9242c79595"
+Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"

From 86e2a5a89d18a1bd09bbfbb5b22f443c041b2c9b Mon Sep 17 00:00:00 2001
From: Reuben Gardos Reid <5456207+ReubenJ@users.noreply.github.com>
Date: Wed, 23 Oct 2024 13:27:00 +0200
Subject: [PATCH 3/3] Test with Aqua

---
 test/runtests.jl | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/test/runtests.jl b/test/runtests.jl
index 45608d0..5b5e867 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -1,6 +1,8 @@
 using HerbSpecification
 using Test
+using Aqua
 
 @testset "HerbSpecification.jl" verbose=true begin
+    @testset "Aqua.jl Checks" Aqua.test_all(HerbSpecification)
     include("test_ioproblem.jl") 
 end