From ff65d1e285a97295708899bebdcc83ec214cd347 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sat, 7 Jan 2023 21:10:30 +0000
Subject: Add containers types.

Containers are syntactic sugar. They are also completely untested.
---
 src/Obs/NormalForm.idr | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'src/Obs/NormalForm.idr')

diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index 0b9d2b6..b4b9f94 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -2,6 +2,7 @@ module Obs.NormalForm
 
 import Data.List.Elem
 
+import Obs.Logging
 import Obs.Pretty
 import Obs.Substitution
 import Obs.Universe
@@ -265,3 +266,11 @@ PointedRename Relevance (\r => Maybe String) NormalForm where
   point {s = Irrelevant} _ _ = Irrel
   point {s = Relevant} var i =
     Ntrl (Var {var = maybe "" id var, i})
+
+-- Useful Constructors ---------------------------------------------------------
+
+public export
+record ContainerTy (ctx : List Relevance) where
+  constructor MkContainerTy
+  inputSort, shapeSort, positionSort, outputSort : Universe
+  input, output : TypeNormalForm ctx
-- 
cgit v1.2.3