From 9af1a41a58575508c8d2dff6e7b25a5caac8aadc Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sun, 8 Jan 2023 00:56:11 +0000 Subject: Add box types. --- src/Obs/NormalForm.idr | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src/Obs/NormalForm.idr') diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr index d325f1a..b290240 100644 --- a/src/Obs/NormalForm.idr +++ b/src/Obs/NormalForm.idr @@ -49,6 +49,8 @@ data Constructor : Unsorted.Family Relevance where Bool : Constructor ctx True : Constructor ctx False : Constructor ctx + Box : (prop : TypeNormalForm ctx) -> Constructor ctx + MkBox : Constructor ctx Top : Constructor ctx Bottom : Constructor ctx @@ -139,6 +141,8 @@ prettyPrecCnstr d (Pair {indexRel, elementRel, prf, first, second}) = prettyPrecCnstr d Bool = pretty "Bool" prettyPrecCnstr d True = pretty "True" prettyPrecCnstr d False = pretty "False" +prettyPrecCnstr d (Box {prop}) = prettyApp d (pretty "Box") [prettyPrec App prop] +prettyPrecCnstr d MkBox = pretty "box" prettyPrecCnstr d Top = pretty "()" prettyPrecCnstr d Bottom = pretty "Void" @@ -224,6 +228,8 @@ renameCnstr (Pair {indexRel, elementRel, prf, first, second}) f = renameCnstr Bool f = Bool renameCnstr True f = True renameCnstr False f = False +renameCnstr (Box {prop}) f = Box {prop = rename prop f} +renameCnstr MkBox f = MkBox renameCnstr Top f = Top renameCnstr Bottom f = Bottom -- cgit v1.2.3