You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: src/Agda2Hs/Compile.hs
+1-2Lines changed: 1 addition & 2 deletions
Original file line number
Diff line number
Diff line change
@@ -116,7 +116,7 @@ compile opts tlm _ def =
116
116
117
117
verifyOutput::
118
118
Options->ModuleEnv->IsMain->TopLevelModuleName
119
-
-> [(CompiledDef, CompileOutput)] ->TCMBool
119
+
-> [(CompiledDef, CompileOutput)] ->TCM()
120
120
verifyOutput _ _ _ m ls =do
121
121
reportSDoc "agda2hs.compile"5$ text "Checking generated output before rendering: "<+> prettyTCM m
122
122
ensureUniqueConstructors
@@ -134,4 +134,3 @@ verifyOutput _ _ _ m ls = do
134
134
duplicateCons =filter ((>1) .length) . group . sort $ allCons
135
135
when (length duplicateCons >0) $
136
136
genericDocError =<< vcat (map (\x -> text $"Cannot generate multiple constructors with the same identifier: "<>Hs.prettyPrint (headWithDefault __IMPOSSIBLE__ x)) duplicateCons)
0 commit comments