git.iko.soy/Idris-dev
on master help sign in
:apropos syntax for binders

Together with space splitting, this lets :apropos be used as a kind of dumber Hoogle. For instance: ``` Idris> :apropos nat -> string Prelude.Strings.length : String -> Nat Returns the length of the string. Idris> :apropos fin -> string Idris> :apropos fin -> plus Idris> :apropos fin -> + Prelude.Fin.+ : Fin n -> Fin m -> Fin (n + m) Add two Fins, extending the bound Prelude.Fin.shift : (m : Nat) -> Fin n -> Fin (m + n) Add some natural number to a Fin, extending the bound accordingly Prelude.Fin.weakenN : (n : Nat) -> Fin m -> Fin (m + n) Weaken the bound on a Fin by some amount ```

commitc8d8a5a31d2173e3f71d4882883c3af89cf95d51 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 4 May 2014, 23:21 (12 years ago) parent7c33668
1 file changed+4−4
compare with master
unifiedsplit
src/Idris/Apropos.hs+4−4
src/Idris/Apropos.hs+4−4
@@ -52,10 +52,10 @@ instance Apropos Def where
5252 isApropos str (CaseOp _ ty ty' _ _ _) = isApropos str ty
5353
5454instance Apropos (Binder (TT Name)) where
55− isApropos str (Lam ty) = isApropos str ty
56− isApropos str (Pi ty) = isApropos str ty
57− isApropos str (Let ty val) = isApropos str ty || isApropos str val
58− isApropos str (NLet ty val) = isApropos str ty || isApropos str val
55+ isApropos str (Lam ty) = str == T.pack "\\" || isApropos str ty
56+ isApropos str (Pi ty) = str == T.pack "->" || isApropos str ty
57+ isApropos str (Let ty val) = str == T.pack "let" || isApropos str ty || isApropos str val
58+ isApropos str (NLet ty val) = str == T.pack "let" || isApropos str ty || isApropos str val
5959 isApropos str _ = False -- these shouldn't occur in defined libraries
6060
6161instance Apropos (TT Name) where