summaryrefslogtreecommitdiff
path: root/src/Obs/Typing/Conversion.idr
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2023-01-07 21:10:30 +0000
committerGreg Brown <greg.brown01@ed.ac.uk>2023-01-07 21:58:30 +0000
commitff65d1e285a97295708899bebdcc83ec214cd347 (patch)
tree7a786ef895ff2dea0ba31b3c7cd7397024214a10 /src/Obs/Typing/Conversion.idr
parentf38761fd38207a6d9a6cc2134384cb7115a5e998 (diff)
Add containers types.
Containers are syntactic sugar. They are also completely untested.
Diffstat (limited to 'src/Obs/Typing/Conversion.idr')
-rw-r--r--src/Obs/Typing/Conversion.idr4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr
index 93812c1..28a3c18 100644
--- a/src/Obs/Typing/Conversion.idr
+++ b/src/Obs/Typing/Conversion.idr
@@ -88,8 +88,8 @@ convertCnstr
pure (convertIndex && convertElement)
convertCnstr
- left@(Pair {indexRel, elementRel, prf = _, first, second})
- right@(Pair
+ (Pair {indexRel, elementRel, prf = _, first, second})
+ (Pair
{ indexRel = indexRel'
, elementRel = elementRel'
, prf = _