Add containers types.

Containers are syntactic sugar. They are also completely untested.

1 files changed, 9 insertions, 0 deletions

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