From 81fc802fa869fa206bfe1bec131639ba3c36b5a8 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 26 Sep 2021 11:11:30 +0200
Subject: [PATCH] move SomeTerm stuff

---
 src/Quox/Eval.idr        | 24 ------------------------
 src/Quox/Syntax/Term.idr | 24 ++++++++++++++++++++++++
 2 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/src/Quox/Eval.idr b/src/Quox/Eval.idr
index e026814..0e3e878 100644
--- a/src/Quox/Eval.idr
+++ b/src/Quox/Eval.idr
@@ -15,30 +15,6 @@ import Data.SortedMap
 %default total
 
 
-public export Exists2 : (ty1 -> ty2 -> Type) -> Type
-Exists2 t = Exists (\a => Exists (\b => t a b))
-
-parameters {0 t : ty -> Type}
-  private %inline some : t a -> Exists t
-  some t = Evidence _ t
-
-parameters {0 t : ty1 -> ty2 -> Type}
-  private %inline some2 : t a b -> Exists2 t
-  some2 t = some $ some t
-
-||| A term of some unknown scope sizes.
-public export SomeTerm : Type
-SomeTerm = Exists2 Term
-
-||| An elimination of some unknown scope sizes.
-public export SomeElim : Type
-SomeElim = Exists2 Elim
-
-||| A dimension of some unknown scope size.
-public export SomeDim : Type
-SomeDim = Exists Dim
-
-
 public export
 record Global where
   constructor G
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index d10d41d..b1441c5 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -368,3 +368,27 @@ parameters {auto _ : Alternative f}
 export
 step' : Elim d n -> Elim d n
 step' e = fromMaybe e $ step e
+
+
+public export Exists2 : (ty1 -> ty2 -> Type) -> Type
+Exists2 t = Exists (\a => Exists (\b => t a b))
+
+parameters {0 t : ty -> Type}
+  public export %inline some : t a -> Exists t
+  some t = Evidence _ t
+
+parameters {0 t : ty1 -> ty2 -> Type}
+  public export %inline some2 : t a b -> Exists2 t
+  some2 t = some $ some t
+
+||| A term of some unknown scope sizes.
+public export SomeTerm : Type
+SomeTerm = Exists2 Term
+
+||| An elimination of some unknown scope sizes.
+public export SomeElim : Type
+SomeElim = Exists2 Elim
+
+||| A dimension of some unknown scope size.
+public export SomeDim : Type
+SomeDim = Exists Dim