From 4b9b6b0211f6fb5691d67ca77ac09be888e569b7 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Thu, 1 Feb 2024 19:25:13 +0000
Subject: Define generic syntax construction.

Whilst it works (see `Example`), a generated data type would probably
work better.
---
 src/SOAS.idr | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'src/SOAS.idr')

diff --git a/src/SOAS.idr b/src/SOAS.idr
index 892f039..9eb7c4c 100644
--- a/src/SOAS.idr
+++ b/src/SOAS.idr
@@ -5,6 +5,7 @@ import public SOAS.Context
 import public SOAS.Family
 import public SOAS.Strength
 import public SOAS.Structure
+import public SOAS.Syntax
 import public SOAS.Theory
 import public SOAS.Var
 
@@ -88,7 +89,3 @@ import public SOAS.Var
 -- prod : (signatures : List $ type.SortedFunctor) ->
 --   type.SortedFunctor
 -- (prod signatures) x ty ctx = All (\sig => sig x ty ctx) signatures
-
-public export
-bind : (tys : type.Ctx) -> type.SortedFunctor
-bind tys = (<<< tys)
-- 
cgit v1.2.3