From dc51e8af17a375d7a07d385ae8f58cdc5f59b488 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 20 Jul 2024 11:04:00 -0700
Subject: [PATCH] pre-binding

---
 src/Lib/Types.idr | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr
index e80d737..7c84543 100644
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -36,6 +36,9 @@ Show Icit where
 public export
 data BD = Bound | Defined
 
+Show BD where
+  show Bound = "bnd"
+  show Defined = "def"
 
 public export
 data Tm : Type where
@@ -157,8 +160,13 @@ Show Val where
   show VU = "U"
 
 
-public export
-data Binder = Bind String BD Val
+-- Not used yet
+data Binder : Type where
+  Bind : (nm : String) -> (bd : BD) -> (val : Val) -> (ty : Val) -> Binder
+
+export covering
+Show Binder where
+  show (Bind nm bd val ty) = "(\{show bd} \{show nm} \{show val} : \{show ty})"
 
 public export
 Env : Type