Skip to content

Commit 41a090d

Browse files
committed
[ re #155 ] Minor simplifications following suggestions by @omelkonian
1 parent 92e1151 commit 41a090d

File tree

2 files changed

+2
-5
lines changed

2 files changed

+2
-5
lines changed

src/Agda2Hs/AgdaUtils.hs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -166,8 +166,7 @@ infoFlags =
166166

167167
resolveStringName :: MonadTCM m => String -> m QName
168168
resolveStringName s = do
169-
cqname <- liftTCM $ parseName noRange s
170-
rname <- liftTCM $ resolveName cqname
169+
rname <- liftTCM $ resolveName =<< parseName noRange s
171170
case rname of
172171
DefinedName _ aname _ -> return $ anameName aname
173172
_ -> liftTCM $ typeError $ CustomBackendError "agda2hs" $ fromString $ "Couldn't find " ++ s

src/Agda2Hs/Compile/Function.hs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -112,9 +112,7 @@ compileFun' withSig def@Defn{..} = inTopContext $ withCurrentModule m $ do
112112
whenM ((withSig &&) <$> inRecordMod defName) $
113113
agda2hsError "not supported: functions inside a record module"
114114

115-
x <- compileQName defName <&> \case
116-
Hs.Qual _ _ x -> x
117-
Hs.UnQual _ x -> x
115+
x <- Hs.unQual <$> compileQName defName
118116

119117
ifM (endsInSort defType)
120118
-- if the function type ends in Sort, it's a type alias!

0 commit comments

Comments
 (0)