idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-02 08:35:07 +03:00
Code Issues Projects Releases Wiki Activity

[ cleanup ] if then else pure () is when

Browse Source
This commit is contained in:
Guillaume ALLAIS 2021-04-28 14:52:54 +01:00 committed by G. Allais
parent afb865f3de
commit 7c5944e811
1 changed files with 5 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/TTImp/Elab/App.idr
View File

@ -319,13 +319,11 @@ mutual
checkPatTyValid fc defs env (NApp _ (NMeta n i _) _) arg got
= do Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)
| Nothing => pure ()
if isErased (multiplicity gdef)
then do -- Argument is only valid if gotnf is not a concrete type
gotnf <- getNF got
if !(concrete defs env gotnf)
then throw (MatchTooSpecific fc env arg)
else pure ()
else pure ()
when (isErased (multiplicity gdef)) $ do
-- Argument is only valid if gotnf is not a concrete type
gotnf <- getNF got
when !(concrete defs env gotnf) $
throw (MatchTooSpecific fc env arg)
checkPatTyValid fc defs env _ _ _ = pure ()
dotErased : {auto c : Ref Ctxt Defs} -> (argty : NF vars) ->