Split monolithic file into modules.

Prove metatheory for generic initial algebras, instead of a clunky
concrete one.

1 files changed, 24 insertions, 0 deletions

diff --git a/src/SOAS/Context.idr b/src/SOAS/Context.idr
new file mode 100644
index 0000000..25d2308
--- /dev/null
+++ b/src/SOAS/Context.idr
@@ -0,0 +1,24 @@
+module SOAS.Context
+
+infixr 4 :-
+
+public export
+record (.extension) (type : Type) where
+  constructor (:-)
+  0 name : String
+  ofType : type
+
+public export
+data (.Ctx) : (type : Type) -> Type where
+  Lin : type.Ctx
+  (:<) : (ctx : type.Ctx) -> (namety : type.extension) -> type.Ctx
+
+public export
+data (.Erased) : type.Ctx -> Type where
+  Z : [<].Erased
+  S : ctx.Erased -> (ctx :< x).Erased
+
+public export
+(++) : (ctx1,ctx2 : type.Ctx) -> type.Ctx
+ctx1 ++ [<] = ctx1
+ctx1 ++ (ctx2 :< ty) = (ctx1 ++ ctx2) :< ty