From d55cf683826376d9f779705fd1dca78791a6805a Mon Sep 17 00:00:00 2001
From: Andre Videla <andre.videla@gmail.com>
Date: Fri, 17 Jan 2025 16:16:30 +0000
Subject: [PATCH] remove TelNames

---
 src/Core/TT/Term.idr | 13 -------------
 1 file changed, 13 deletions(-)

diff --git a/src/Core/TT/Term.idr b/src/Core/TT/Term.idr
index b104fe2421..94f7b9dad8 100644
--- a/src/Core/TT/Term.idr
+++ b/src/Core/TT/Term.idr
@@ -557,19 +557,6 @@ covering
                         assert_total (showSep " " (map show args))
                      ++ ")"
 
-||| A telescope of names and their associated types/terms
-public export
-data TelNames : List Name -> Type where
-  Nil : TelNames xs
-  AddName : (n : Name) -> Term vars -> (isImplicit : Bool) -> TelNames (n :: vars) -> TelNames vars
-
-covering export
-{vars : _} -> Show (TelNames vars) where
-  show [] = ""
-  show (AddName n ty _ []) = "(\{show n} : \{show ty})"
-  show (AddName n ty False rest) = "(\{show n} : \{show ty}) -> \{show rest}"
-  show (AddName n ty True rest) = "{\{show n} : \{show ty}} -> \{show rest}"
-
 ||| Obtain the telescope of names and their types
 export
 collectPiNames : Term vars -> List (Bool, Name)