[ refactor ] Remove redundant Bool output from verifyOutput

agda · Jan 6, 2025 · e47a4f1 · e47a4f1
1 parent f8b84cb
commit e47a4f1
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/src/Agda2Hs/Compile.hs b/src/Agda2Hs/Compile.hs
@@ -116,7 +116,7 @@ compile opts tlm _ def =
 
 verifyOutput ::
   Options -> ModuleEnv -> IsMain -> TopLevelModuleName
-  -> [(CompiledDef, CompileOutput)] -> TCM Bool
+  -> [(CompiledDef, CompileOutput)] -> TCM ()
 verifyOutput _ _ _ m ls = do
   reportSDoc "agda2hs.compile" 5 $ text "Checking generated output before rendering: " <+> prettyTCM m
   ensureUniqueConstructors
@@ -134,4 +134,3 @@ verifyOutput _ _ _ m ls = do
           duplicateCons = filter ((> 1) . length) . group . sort  $ allCons
       when (length duplicateCons > 0) $
         genericDocError =<< vcat (map (\x -> text $ "Cannot generate multiple constructors with the same identifier: " <> Hs.prettyPrint (headWithDefault __IMPOSSIBLE__ x)) duplicateCons)
-      return (length duplicateCons == 0)