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/Total/Reduction.idr | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/Total/Reduction.idr')

diff --git a/src/Total/Reduction.idr b/src/Total/Reduction.idr
index 4870f30..cb13706 100644
--- a/src/Total/Reduction.idr
+++ b/src/Total/Reduction.idr
@@ -95,3 +95,8 @@ wknStep (RecCong2 step) = RecCong2 (wknStep step)
 wknStep (RecCong3 step) = RecCong3 (wknStep step)
 wknStep RecZero = RecZero
 wknStep RecSuc = RecSuc
+
+export
+wknSteps : t >= u -> wkn t thin >= wkn u thin
+wknSteps [<] = [<]
+wknSteps (steps :< step) = wknSteps steps :< wknStep step
-- 
cgit v1.2.3