From 8006ae4c401c75a257891408482b3b9d3cbf19e2 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 27 Feb 2022 01:31:52 +0100
Subject: [PATCH] add DimEqs.zeroEq

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

diff --git a/src/Quox/Syntax/DimEq.idr b/src/Quox/Syntax/DimEq.idr
index b1327c4..dc703b8 100644
--- a/src/Quox/Syntax/DimEq.idr
+++ b/src/Quox/Syntax/DimEq.idr
@@ -25,6 +25,10 @@ data DimEq : Nat -> Type where
 %name DimEq eqs
 
 
+export
+zeroEq : DimEq 0
+zeroEq = C [<]
+
 export
 new' : (d : Nat) -> DimEq' d
 new' 0     = [<]