From 6590816a835110b8181472a5116dd4ecf67c957c Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 6 Jun 2023 15:13:22 +0100
Subject: Add a pretty printer.

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

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

diff --git a/src/Total/Syntax.idr b/src/Total/Syntax.idr
index 6a61cf5..084ae3e 100644
--- a/src/Total/Syntax.idr
+++ b/src/Total/Syntax.idr
@@ -20,6 +20,11 @@ data Len : SnocList Ty -> Type where
 
 %name Len k, m, n
 
+public export
+Cast (Len ctx) Nat where
+  cast Z = 0
+  cast (S k) = S (cast k)
+
 public export
 0 Fun : Len tys -> (Ty -> Type) -> Type -> Type
 Fun Z arg ret = ret
-- 
cgit v1.2.3