From 5560cb67089c9c4f4d07009374379bee292762ef Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 26 Mar 2023 16:14:58 +0200
Subject: [PATCH] move 'enum' to Syntax.Base

---
 lib/Quox/Syntax/Term/Base.idr | 4 ++++
 tests/Tests/PrettyTerm.idr    | 3 ---
 tests/Tests/Typechecker.idr   | 3 ---
 3 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 1929fb4..8414f74 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -234,3 +234,7 @@ BV i = B $ V i
 public export %inline
 BVT : (i : Nat) -> (0 _ : LT i n) => Term q d n
 BVT i = E $ BV i
+
+public export
+enum : List TagVal -> Term q d n
+enum = Enum . SortedSet.fromList
diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr
index ff917ab..ddcacff 100644
--- a/tests/Tests/PrettyTerm.idr
+++ b/tests/Tests/PrettyTerm.idr
@@ -24,9 +24,6 @@ parameters (ds : NContext d) (ns : NContext n)
                  {default str label : String} -> Test
   testPrettyE1 e str {label} = testPrettyT1 (E e) str {label}
 
-enum : List TagVal -> Term q d n
-enum = Enum . SortedSet.fromList
-
 export
 tests : Test
 tests = "pretty printing terms" :- [
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index 977d99d..3c3e68b 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -160,9 +160,6 @@ failing "Can't find an implementation"
   sany : SQty Three
   sany = Element Any %search
 
-enum : List TagVal -> Term q d n
-enum = Enum . SortedSet.fromList
-
 
 export
 tests : Test