From 3107ee7777b0709997975e28d9ef2a46bca8ca47 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 7 Dec 2022 12:32:59 +0000
Subject: Lift index of varFunc.

---
 src/Soat/SecondOrder/Algebra.idr | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/Soat/SecondOrder/Algebra.idr')

diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index e52c945..038e065 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -155,8 +155,8 @@ public export
   }
 
 public export
-(.varFunc) : (a : Algebra sig) -> (ctx : _) -> irrelevantCast (flip Elem ctx) ~> a.setoidAt ctx
-(.varFunc) a ctx = mate (\_ => a.raw.var)
+(.varFunc) : (a : Algebra sig) -> irrelevantCast (uncurry Elem) ~> a.setoid
+(.varFunc) a = mate (\(_, _) => a.raw.var)
 
 public export
 (.substFunc) : (a : Algebra sig) -> (t : _) -> (ctx, ctx' : _)
-- 
cgit v1.2.3