Slight relaxation of proof search rules
Search if there's a function in a constructor index too, don't require
it to be a constructor, since this should be enough to discriminate.
commitd3b66cd420654efc4592afa20415579f1e18835f
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 31 Aug 2015, 20:13 (11 years ago)
parent55ffc21
src/Idris/ProofSearch.hs+3−1
@@ -333,7 +333,9 @@ checkConstructor ist (n : ns) =
333333 where
334334 conIndexed t = let (_, args) = unApply (getRetTy t) in
335335 any conHead args
336− conHead t | (P _ n _, _) <- unApply t = isConName n (tt_ctxt ist)
336+ conHead t | (P _ n _, _) <- unApply t = case lookupDefExact n (tt_ctxt ist) of
337+ Just _ -> True
338+ _ -> False
337339 | otherwise = False
338340
339341-- | Resolve type classes. This will only pick up 'normal' instances, never