diff options
Diffstat (limited to 'src/Obs/NormalForm.idr')
| -rw-r--r-- | src/Obs/NormalForm.idr | 9 |
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 |