From 140ca797c7576253b0a85ce858bd2956cdf1c271 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Oct 2024 08:45:49 -0500
Subject: [PATCH] Regression

---
 tests/CMakeLists.txt         |  1 +
 tests/overload-standalone.eo | 14 ++++++++++++++
 2 files changed, 15 insertions(+)
 create mode 100644 tests/overload-standalone.eo

diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
index 612dd40..6d5913d 100644
--- a/tests/CMakeLists.txt
+++ b/tests/CMakeLists.txt
@@ -126,6 +126,7 @@ set(ethos_test_file_list
     simple-reference.eo
     simple-quant-reference.eo
     simple-lra-reference.eo
+    overload-standalone.eo
 )
 
 if(ENABLE_ORACLES)
diff --git a/tests/overload-standalone.eo b/tests/overload-standalone.eo
new file mode 100644
index 0000000..8fb5a33
--- /dev/null
+++ b/tests/overload-standalone.eo
@@ -0,0 +1,14 @@
+(declare-const or (-> Bool Bool Bool) :right-assoc-nil false)
+(declare-const = (-> (! Type :var T :implicit) T T Bool))
+
+(declare-const a Bool)
+(declare-const b Bool)
+
+(define singleton-list ((T Type :implicit) (f (-> T T T)) (a T)) (eo::cons f a (eo::nil f)))
+
+(declare-rule refl ((T Type) (t T))
+  :args (t)
+  :conclusion (= t t)
+)
+
+(step @p0 (= (or b) (or b)) :rule refl :args ((singleton-list or b)))