From f0f44fe7815435836bc625e837e891188ae8d801 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Mon, 22 Jan 2024 12:11:20 +0000
Subject: Fix some bug?

I don't really know. I haven't read this in a long time.
---
 src/Encoded/Vect.idr | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'src/Encoded/Vect.idr')

diff --git a/src/Encoded/Vect.idr b/src/Encoded/Vect.idr
index 064de5f..e86abdb 100644
--- a/src/Encoded/Vect.idr
+++ b/src/Encoded/Vect.idr
@@ -1,6 +1,7 @@
 module Encoded.Vect
 
 import Data.String
+import Data.Vect
 
 import Encoded.Bool
 import Encoded.Pair
@@ -56,3 +57,13 @@ foldr {k = S k} = Abs $ Abs $ Abs $
   let c = Var (There Here) in
   let xs = Var Here in
   App c [<App xs [<zero], App foldr [<z, c, xs . suc]]
+
+export
+fromVect : {k : Nat} -> {ty : Ty} -> Vect k (Term ty ctx) -> Term (Vect k ty) ctx
+fromVect [] = nil
+fromVect (t :: ts) = App cons [<t, fromVect ts]
+
+export
+toVect : {k : Nat} -> {ty : Ty} -> Term (Vect k ty) ctx -> Vect k (Term ty ctx)
+toVect {k = 0} v = []
+toVect {k = S k} v = App v [<zero] :: toVect (v . suc)
-- 
cgit v1.2.3