From 6dde244c14410ede6d41e9a8607016e23c19e320 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Thu, 1 Feb 2024 15:23:47 +0000
Subject: Split monolithic file into modules.

Prove metatheory for generic initial algebras, instead of a clunky
concrete one.
---
 src/SOAS/Context.idr | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 src/SOAS/Context.idr

(limited to 'src/SOAS/Context.idr')

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
-- 
cgit v1.2.3