Skip to content

Commit 01cc053

Browse files
nauckeliesnikov
authored andcommitted
Use OverloadedStrings in Compile/Record.hs too
1 parent 7ff173b commit 01cc053

File tree

1 file changed

+5
-5
lines changed

1 file changed

+5
-5
lines changed

src/Agda2Hs/Compile/Record.hs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ compileMinRecords def sls = do
8888
| all (x ==) xs = return x
8989
| otherwise = agda2hsErrorM $ do
9090
text ("Conflicting default implementations for " ++ pp f ++ ":") $$
91-
vcat [ text "-" <+> multilineText (pp d) | d <- nub (x : xs) ]
91+
vcat [ "-" <+> multilineText (pp d) | d <- nub (x : xs) ]
9292
decls <- Map.traverseWithKey getUnique
9393
$ Map.unionsWith (<>) $ (map . fmap) (:| []) defaults
9494

@@ -183,17 +183,17 @@ checkUnboxPragma def = do
183183
-- recRecursive can be used again after agda 2.6.4.2 is released
184184
-- see agda/agda#7042
185185
unless (all null recMutual) $ agda2hsErrorM $
186-
text "Unboxed record" <+> prettyTCM (defName def)
187-
<+> text "cannot be recursive"
186+
"Unboxed record" <+> prettyTCM (defName def)
187+
<+> "cannot be recursive"
188188

189189
TelV tel _ <- telViewUpTo recPars (defType def)
190190
addContext tel $ do
191191
pars <- getContextArgs
192192
let fieldTel = recTel `apply` pars
193193
fields <- nonErasedFields fieldTel
194194
unless (length fields == 1) $ agda2hsErrorM $
195-
text "Unboxed record" <+> prettyTCM (defName def)
196-
<+> text "should have exactly one non-erased field"
195+
"Unboxed record" <+> prettyTCM (defName def)
196+
<+> "should have exactly one non-erased field"
197197

198198
where
199199
nonErasedFields :: Telescope -> C [String]

0 commit comments

Comments
 (0)