Define Vars.

1 files changed, 41 insertions, 0 deletions

diff --git a/src/Core/Var.idr b/src/Core/Var.idr
new file mode 100644
index 0000000..502a416
--- /dev/null
+++ b/src/Core/Var.idr
@@ -0,0 +1,41 @@
+module Core.Var
+
+import Core.Context
+
+-- Variables -------------------------------------------------------------------
+
+data IsVar : Nat -> Context -> Type where
+  Here : IsVar 0 (sx :< n)
+  There : IsVar k sx -> IsVar (S k) (sx :< n)
+
+export
+record Var (sx : Context) where
+  constructor MakeVar
+  index : Nat
+  0 prf : IsVar index sx
+
+%name IsVar prf
+%name Var i, j, k
+
+-- Constructors ----------------------------------------------------------------
+
+export
+here : Var (sx :< n)
+here = MakeVar 0 Here
+
+export
+there : Var sx -> Var (sx :< n)
+there (MakeVar index prf) = MakeVar (S index) (There prf)
+
+-- Views -----------------------------------------------------------------------
+
+namespace View
+  public export
+  data View : Var sx -> Type where
+    Here : View Core.Var.here
+    There : (i : Var sx) -> View (there i)
+
+export
+view : (i : Var sx) -> View i
+view (MakeVar 0 Here) = Here
+view (MakeVar (S k) (There prf)) = There (MakeVar k prf)