From bf07a9fe3ee4ff06fe186e33221f7f91871b9217 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 6 Jun 2023 12:25:26 +0100
Subject: Write an encoding for data types.

---
 src/Thinning.idr | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/Thinning.idr')

diff --git a/src/Thinning.idr b/src/Thinning.idr
index a79f0f5..a9b724d 100644
--- a/src/Thinning.idr
+++ b/src/Thinning.idr
@@ -31,6 +31,11 @@ keep Id = Id
 keep (Drop thin) = Keep (Drop thin)
 keep (Keep thin) = Keep (Keep thin)
 
+public export
+empty : (sx : SnocList a) -> [<] `Thins` sx
+empty [<] = Id
+empty (sx :< x) = Drop (empty sx)
+
 -- Operations ------------------------------------------------------------------
 
 public export
-- 
cgit v1.2.3