diff options
Diffstat (limited to 'src/Obs/Typing')
| -rw-r--r-- | src/Obs/Typing/Conversion.idr | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr index 28a3c18..0e65790 100644 --- a/src/Obs/Typing/Conversion.idr +++ b/src/Obs/Typing/Conversion.idr @@ -105,6 +105,9 @@ convertCnstr convertCnstr Bool Bool = pure True convertCnstr True True = pure True convertCnstr False False = pure True +convertCnstr (Box {prop}) (Box {prop = prop'}) = + convert {rel = Relevant, type = cast Prop, left = prop, right = prop'} +convertCnstr MkBox MkBox = pure True convertCnstr Top Top = pure True convertCnstr Bottom Bottom = pure True convertCnstr left right = pure False @@ -200,6 +203,7 @@ convertEta (Pair {indexRel = Relevant, elementRel = Irrelevant, prf, first, seco convertEta (Pair {indexRel = Irrelevant, elementRel = Relevant, prf, first, second}) right = do let rightSecond = Second {firstRel = Relevant, arg = right} convertUntyped {rel = Relevant, left = second, right = Ntrl rightSecond} +convertEta MkBox right = pure True convertEta left right = pure False convertUntyped Irrelevant left right = pure True |