Skip to content

Commit b26e677

Browse files
committed
Remove redundant forced pattern check
Actually, given we check for dotted patterns earlier in compileClause', I don't think there is any need to checkNonErasedForced in compilePats?
1 parent c66a5bc commit b26e677

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

src/Agda2Hs/Compile/Function.hs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -297,7 +297,6 @@ compilePats ty ((namedArg -> pat):ps) = do
297297
(a, b) <- mustBePi ty
298298
reportSDoc "agda2hs.compile.pattern" 10 $ text "Compiling pattern:" <+> prettyTCM pat
299299
let rest = compilePats (absApp b (patternToTerm pat)) ps
300-
checkNonErasedForced a pat
301300
compileDom a >>= \case
302301
DOInstance -> rest
303302
DODropped -> rest

0 commit comments

Comments
 (0)