@@ -1746,10 +1746,27 @@ addImpl' inpat env infns imp_meths ist ptm
1746 = PWithApp fc (ai inpat qq env ds f) (ai inpat qq env ds a)
1746 = PWithApp fc (ai inpat qq env ds f) (ai inpat qq env ds a)
1747 ai inpat qq env ds (PCase fc c os)
1747 ai inpat qq env ds (PCase fc c os)
1748 = let c' = ai inpat qq env ds c in
1748 = let c' = ai inpat qq env ds c in
1749− -- leave os alone, because they get lifted into a new pattern match
1749+ -- leave lhs alone, because they get lifted into a new pattern match
1750− -- definition which is passed through addImpl agai inpatn with more scope
1750+ -- definition which is passed through addImpl again
1752− PCase fc c' os
1751+ PCase fc c' (map aiCase os)
1754+ = (lhs, ai inpat qq (env ++ patnames lhs) ds rhs)
1756+ -- Anything beginning with a lower case letter, not applied,
1757+ -- and no namespace is a pattern variable
1758+ patnames (PApp _ (PRef _ _ f) [])
1759+ | implicitable f = [(f, Nothing)]
1760+ patnames (PRef _ _ f)
1761+ | implicitable f = [(f, Nothing)]
1762+ patnames (PApp _ (PRef _ _ _) args)
1763+ = concatMap patnames (map getTm args)
1764+ patnames (PPair _ _ _ l r) = patnames l ++ patnames r
1765+ patnames (PDPair _ _ _ l t r) = patnames l ++ patnames t ++ patnames r
1766+ patnames (PAs _ _ t) = patnames t
1767+ patnames (PAlternative _ _ ts) = concatMap patnames ts
1754 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1771 ai inpat qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai inpat qq env ds c)
1755 (ai inpat qq env ds t)
1772 (ai inpat qq env ds t)