git.iko.soy/Idris-dev
on master help sign in
:apropos syntax for binders
c8d8a5aDavid Raymond Christiansen
src/Idris/Apropos.hs+4−4
compare with master
unifiedsplit
@@ -52,10 +52,10 @@ instance Apropos Def where
52 isApropos str (CaseOp _ ty ty' _ _ _) = isApropos str ty
52 isApropos str (CaseOp _ ty ty' _ _ _) = isApropos str ty
53
53
54instance Apropos (Binder (TT Name)) where
54instance Apropos (Binder (TT Name)) where
55− isApropos str (Lam ty) = isApropos str ty
55+ isApropos str (Lam ty) = str == T.pack "\\" || isApropos str ty
56− isApropos str (Pi ty) = isApropos str ty
56+ isApropos str (Pi ty) = str == T.pack "->" || isApropos str ty
57− isApropos str (Let ty val) = isApropos str ty || isApropos str val
57+ isApropos str (Let ty val) = str == T.pack "let" || isApropos str ty || isApropos str val
58− isApropos str (NLet ty val) = isApropos str ty || isApropos str val
58+ isApropos str (NLet ty val) = str == T.pack "let" || isApropos str ty || isApropos str val
59 isApropos str _ = False -- these shouldn't occur in defined libraries
59 isApropos str _ = False -- these shouldn't occur in defined libraries
60
60
61instance Apropos (TT Name) where
61instance Apropos (TT Name) where