move SomeTerm stuff

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

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