From 4da8aa6031a4dcf3d2ec04c3b23ed754e46be639 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 9 Sep 2021 23:56:29 +0200
Subject: [PATCH] start of eval module but not really

---
 src/Quox/Eval.idr | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 src/Quox/Eval.idr

diff --git a/src/Quox/Eval.idr b/src/Quox/Eval.idr
new file mode 100644
index 0000000..ba1e892
--- /dev/null
+++ b/src/Quox/Eval.idr
@@ -0,0 +1,30 @@
+module Quox.Eval
+
+-- todo list:
+-- - understand nbe and use it
+-- - take a proof of well-typedness as an argument
+
+import Quox.Syntax
+
+import Data.DPair
+
+%default total
+
+
+public export Exists2 : (ty1 -> ty2 -> Type) -> Type
+Exists2 t = Exists (\a => Exists (\b => t a b))
+
+public export SomeTerm : Type
+SomeTerm = Exists2 Term
+
+public export SomeElim : Type
+SomeElim = Exists2 Elim
+
+public export SomeDim : Type
+SomeDim = Exists Dim
+
+private some : {0 t : ty -> Type} -> t a -> Exists t
+some t = Evidence ? t
+
+private some2 : {0 t : ty1 -> ty2 -> Type} -> t a b -> Exists2 t
+some2 t = some $ some t