From e258c78a5ab9529242b4c8fa168eda85430e641e Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Mon, 28 Oct 2024 15:34:16 +0000
Subject: Make everything relevant.

Too few proofs were relevant. Now they are.
---
 src/Inky/Data/Thinned.idr | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 src/Inky/Data/Thinned.idr

(limited to 'src/Inky/Data/Thinned.idr')

diff --git a/src/Inky/Data/Thinned.idr b/src/Inky/Data/Thinned.idr
new file mode 100644
index 0000000..6ee0d50
--- /dev/null
+++ b/src/Inky/Data/Thinned.idr
@@ -0,0 +1,18 @@
+module Inky.Data.Thinned
+
+import public Inky.Data.SnocList.Thinning
+
+public export
+record Thinned (0 p : SnocList a -> Type) (ctx : SnocList a) where
+  constructor Over
+  {0 support : SnocList a}
+  value : p support
+  thins : support `Thins` ctx
+
+public export
+rename : (ctx1 `Thins` ctx2) -> Thinned p ctx1 -> Thinned p ctx2
+rename f (value `Over` thins) = value `Over` (f . thins)
+
+public export
+(.extract) : Rename a p => Thinned p ctx -> p ctx
+(value `Over` thins).extract = rename thins value
-- 
cgit v1.2.3