Another small reduction in calls to TT.(==)
commitba1525769c2c2ad316fe8d07c4497482c83497b9
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateThu 16 Jan 2014, 10:47 (13 years ago)
parenta7859f6
src/Idris/Core/ProofState.hs+1−1
@@ -747,7 +747,7 @@ updateSolved' xs (Bind n (Hole ty) t)
747747updateSolved' xs (Bind n b t)
748748 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
749749updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)
750−updateSolved' xs (P _ n _)
750+updateSolved' xs (P _ n@(MN _ _) _)
751751 | Just v <- lookup n xs = v
752752updateSolved' xs t = t
753753