summaryrefslogtreecommitdiff
path: root/src/SOAS.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/SOAS.idr')
-rw-r--r--src/SOAS.idr5
1 files changed, 1 insertions, 4 deletions
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)