git.iko.soy/Idris-dev
on master help sign in
Another small reduction in calls to TT.(==)
ba15257Edwin Brady
src/Idris/Core/ProofState.hs+1−1
compare with master
unifiedsplit
@@ -747,7 +747,7 @@ updateSolved' xs (Bind n (Hole ty) t)
747updateSolved' xs (Bind n b t)
747updateSolved' xs (Bind n b t)
748 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
748 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
749updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)
749updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)
750−updateSolved' xs (P _ n _)
750+updateSolved' xs (P _ n@(MN _ _) _)
751 | Just v <- lookup n xs = v
751 | Just v <- lookup n xs = v
752updateSolved' xs t = t
752updateSolved' xs t = t
753
753