diff options
Diffstat (limited to 'src/Obs/Typing')
| -rw-r--r-- | src/Obs/Typing/Conversion.idr | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr index 20198c5..37bdf67 100644 --- a/src/Obs/Typing/Conversion.idr +++ b/src/Obs/Typing/Conversion.idr @@ -42,6 +42,11 @@ convert t u (Cnstr (Sigma s s' var a b)) (Set k) = do convert t2 u2 b s' -- In type Sum (manually expanding definition of doCase) convert t u (Cnstr (Sum s s' a b)) (Set _) = convertSum t u s s' a b +-- In type Container +convert t u (Cnstr (Container s a s' s'')) (Set l) = do + t <- expandContainer t + u <- expandContainer u + convert (Cnstr t) (Cnstr u) (Cnstr (expandContainerTy s a s' s'')) (Set l) -- Default convert t u a s = inScope "invalid conversion" $ fatal $ @@ -57,6 +62,9 @@ convertSet (Cnstr (Sigma s s' _ a b)) (Cnstr (Sigma l l' _ a' b')) = convertSet (Cnstr (Sum s s' a b)) (Cnstr (Sum l l' a' b')) = pure $ s == l && s' == l' && !(convertSet a a') && !(convertSet b b') +convertSet (Cnstr (Container s a s' s'')) (Cnstr (Container l a' l' l'')) = + pure $ + s == l && s' == l' && s'' == l'' && !(convertSet a a') convertSet (Cnstr Top) (Cnstr Top) = pure True convertSet (Cnstr Bottom) (Cnstr Bottom) = pure True convertSet (Ntrl t) u = pure (Ntrl t == u) |