diff options
Diffstat (limited to 'src/Obs/NormalForm.idr')
| -rw-r--r-- | src/Obs/NormalForm.idr | 6 |
1 files changed, 6 insertions, 0 deletions
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 |