From e6d942ce1bcec78933b80fa0d830e0991bee67d0 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Wed, 6 Apr 2022 20:32:56 +0200
Subject: [PATCH] add Dim.toConst

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

diff --git a/src/Quox/Syntax/Dim.idr b/src/Quox/Syntax/Dim.idr
index 5fe0cbf..57b8b88 100644
--- a/src/Quox/Syntax/Dim.idr
+++ b/src/Quox/Syntax/Dim.idr
@@ -50,6 +50,11 @@ PrettyHL (Dim n) where
   prettyM (B i) = prettyVar DVar DVarErr (!ask).dnames i
 
 
+public export %inline
+toConst : Dim 0 -> DimConst
+toConst (K e) = e
+
+
 public export
 DSubst : Nat -> Nat -> Type
 DSubst = Subst Dim