From 9e2bd48420feba7c7752fd98cdf10fb67f56edc8 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 15 Apr 2023 17:07:32 +0100
Subject: Define declarative typing rules.

---
 src/Core/Term/Thinned.idr | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/Core/Term')

diff --git a/src/Core/Term/Thinned.idr b/src/Core/Term/Thinned.idr
index 824439a..3ed4779 100644
--- a/src/Core/Term/Thinned.idr
+++ b/src/Core/Term/Thinned.idr
@@ -20,6 +20,11 @@ record Thinned (n : Nat) where
 
 %name Thinned t, u, v
 
+%inline
+public export
+pure : Term n -> Thinned n
+pure = (`Over` id n)
+
 %inline
 public export
 expand : Thinned n -> Term n
-- 
cgit v1.2.3