From bfba6b295a8cdf7321d939f22fbdd04d45408e63 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Thu, 12 Jan 2023 17:56:11 +0000
Subject: Fix bug in equality for pi types.

---
 src/Obs/NormalForm/Normalise.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/Obs/NormalForm')

diff --git a/src/Obs/NormalForm/Normalise.idr b/src/Obs/NormalForm/Normalise.idr
index 28d66da..3ed0e67 100644
--- a/src/Obs/NormalForm/Normalise.idr
+++ b/src/Obs/NormalForm/Normalise.idr
@@ -505,7 +505,7 @@ equalHelper
   let returnElement = Cnstr $ Pi
        { domainSort = domainSort
        , codomainSort = Prop
-       , domain = MkDecl Nothing (Sorted.weaken [Irrelevant] domain.type)
+       , domain = MkDecl Nothing (Sorted.weaken [Irrelevant] domain'.type)
        , codomain = codomainEqual
        }
 
-- 
cgit v1.2.3