From 8dfd872384d32998886d9938f9c741002fd47253 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 26 Jan 2024 15:14:48 +0000
Subject: Remove runtime dependency on the context.

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

(limited to 'src/SOAS.idr')

diff --git a/src/SOAS.idr b/src/SOAS.idr
index befd53c..8540c83 100644
--- a/src/SOAS.idr
+++ b/src/SOAS.idr
@@ -136,12 +136,12 @@ record MonStruct (m : type.SortedFamily) where
   var : Var -|> m
   mult : m -|> (m ^ m)
 
-(.sub) : {m : type.SortedFamily} -> {ty,sy : type} -> {ctx : type.Ctx} ->
+(.sub) : {m : type.SortedFamily} -> {ty,sy : type} -> {0 ctx : type.Ctx} ->
   (mon : MonStruct m) => m sy (ctx :< (n :- ty)) -> m ty ctx -> m sy ctx
 t.sub s = mon.mult t (extend m s mon.var)
 
 (.sub2) : {m : type.SortedFamily} -> {ty1,ty2,sy : type} ->
-  {ctx : type.Ctx} ->
+  {0 ctx : type.Ctx} ->
   (mon : MonStruct m) => m sy (ctx :< (x :- ty1) :< (x :- ty2)) ->
   m ty1 ctx ->  m ty2 ctx -> m sy ctx
 t.sub2 s1 s2 = mon.mult t (extend m s2 (extend m s1 mon.var))
-- 
cgit v1.2.3