From 3722c769cf915b06fb262e15a80ec478b7860fe6 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 27 Feb 2022 01:50:01 +0100
Subject: [PATCH] add some properties of Var.Compare

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

diff --git a/src/Quox/Syntax/Var.idr b/src/Quox/Syntax/Var.idr
index 7f52766..08bc166 100644
--- a/src/Quox/Syntax/Var.idr
+++ b/src/Quox/Syntax/Var.idr
@@ -185,6 +185,16 @@ compareP VZ     (VS j) = IsLT LTZ
 compareP (VS i) VZ     = IsGT LTZ
 compareP (VS i) (VS j) = compareS $ compareP i j
 
+export
+0 compareSelf : (c : Compare i i) -> c = IsEQ
+compareSelf (IsLT lt) = absurd lt
+compareSelf IsEQ      = Refl
+compareSelf (IsGT gt) = absurd gt
+
+export
+0 comparePSelf : (i : Var n) -> compareP i i = IsEQ
+comparePSelf i = compareSelf {}
+
 
 public export
 data LTE : Var n -> Var n -> Type where