<div dir="ltr">OK, I've made it work. I used copy and paste from<div><br></div><div> <a href="http://www.cse.chalmers.se/~nad/listings/lib/Everything.html" target="_blank" style="color:rgb(17,85,204);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255)">http://www.cse.chalmers.<wbr>se/~nad/listings/lib/<wbr>Everything.html</a></div><div><br></div><div>and then changed all occurrences of "import" to "open import", and then using ^C ^Z does indeed work. It produces a large and difficult to read listing (because it finds many entries with huge types), but is much better than what I had previously (which was to guess where to look).</div><div><br></div><div>Thank you to all for your help. If someone did produce Hoogle for Agda, it would be a huge boon. Cheers, -- P</div></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 15 February 2018 at 17:07, Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Thank you! Everything sounds like everything I need!<div><br></div><div>I got the standard library from here:</div><div><br></div><div> git clone <a href="https://github.com/agda/agda-stdlib.git" target="_blank">https://github.com/agda/<wbr>agda-stdlib.git</a> ~/agda-stdlib</div><div><br></div><div>This version does not have a file called Everything. It has no Makefile that I can spot. It does contain a file called GenerateEverything.hs, but it doesn't work for me:</div><div><br></div><div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">bruichladdich$ ghci GenerateEverything.hs <br>GHCi, version 8.2.2: <a href="http://www.haskell.org/ghc/" target="_blank">http://www.haskell.org/ghc/</a> :? for help<br>[1 of 1] Compiling Main ( GenerateEverything.hs, interpreted )<br>GenerateEverything.hs:9:1: error:<br> Could not find module ‘System.FilePath.Find’<br> Perhaps you meant<br> System.FilePath.Windows (from filepath-1.4.1.2)<br> System.FilePath (from filepath-1.4.1.2)<br> System.FilePath.Posix (from filepath-1.4.1.2)<br> Use -v to see a list of the files searched for.<br> |<br>9 | import System.FilePath.Find<br> | ^^^^^^^^^^^^^^^^^^^^^^^^^^^<br>Failed, no modules loaded.<br>Prelude> </blockquote><div><br></div><div>What are my other options? Could someone simply add Everything.agda to <a href="https://github.com/agda/agda-stdlib.git" style="color:rgb(17,85,204);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255)" target="_blank">https://github.com/agda/agd<wbr>a-stdlib.git</a>, and then I could pull it?</div><div><br></div><div>Cheers, -- P</div><blockquote type="cite" style="color:rgb(80,0,80);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial"><div class="gmail_extra"><div class="gmail_quote"><div><span style="font-size:small;color:rgb(34,34,34)"> </span><br></div></div></div></blockquote></div></div><div class="gmail_extra"><span class=""><br clear="all"><div><div class="m_-2587342160859142376gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div></div></div></div></div>
<br></span><div><div class="h5"><div class="gmail_quote">On 15 February 2018 at 14:23, Liam O'Connor <span dir="ltr"><<a href="mailto:liamoc@cse.unsw.edu.au" target="_blank">liamoc@cse.unsw.edu.au</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space"><div id="m_-2587342160859142376m_-7173118898084949436bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px;color:rgba(0,0,0,1.0);margin:0px;line-height:auto"><br></div> The agda standard library has a makefile entry for an “Everything.agda” that includes.. well… everything in the standard library.<div><br></div><div>You can build that file, and it should suit your purposes. (It has a listing here <a href="http://www.cse.chalmers.se/~nad/listings/lib/Everything.html" target="_blank">http://www.cse.chalmers.s<wbr>e/~nad/listings/lib/Everything<wbr>.html</a>)</div><div><br> <div class="m_-2587342160859142376m_-7173118898084949436bloop_sign" id="m_-2587342160859142376m_-7173118898084949436bloop_sign_1518711709732366080"></div><div id="m_-2587342160859142376m_-7173118898084949436bloop_sign_1518711709732366080" class="m_-2587342160859142376m_-7173118898084949436bloop_sign">Regards,</div><div id="m_-2587342160859142376m_-7173118898084949436bloop_sign_1518711709732366080" class="m_-2587342160859142376m_-7173118898084949436bloop_sign">Liam</div><div><div class="m_-2587342160859142376h5"> <br><p class="m_-2587342160859142376m_-7173118898084949436airmail_on">On 16 February 2018 at 3:19:04 am, Philip Wadler (<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>) wrote:</p> <blockquote type="cite" class="m_-2587342160859142376m_-7173118898084949436clean_bq"><span><div><div></div><div>
<div dir="ltr">Thanks!
<div><br></div>
<div>What would help enormously is if I could do the same thing,
*searching the entire standard library*. This basically requires
someone to put together a huge import list and put it in a file
(preferably available with the standard library). Has anyone done
so, or could this be whipped together quickly?</div>
<div><br></div>
<div>Cheers, -- P</div>
</div>
<div class="gmail_extra"><br clear="all">
<div>
<div class="m_-2587342160859142376m_-7173118898084949436gmail_signature" data-smartmail="gmail_signature">
<div dir="ltr">
<div>
<div dir="ltr">. \ Philip Wadler, Professor of Theoretical
Computer Science,<br>
. /\ School of Informatics, University of
Edinburgh<br></div>
<div>. / \ and Senior Research Fellow, IOHK<br></div>
<div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div>
</div>
</div>
</div>
</div>
<br>
<div class="gmail_quote">On 15 February 2018 at 14:01, Guillaume
Allais <span dir="ltr"><<a href="mailto:guillaume.allais@ens-lyon.org" target="_blank">guillaume.allais@ens-lyon.org</a><wbr>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div text="#000000" bgcolor="#FFFFFF"><tt>Hi Phil,<br>
<br>
There's a *very basic* search functionality which you can
invoke<br>
from emacs using C-c C-z. You can then input a
space-separated<br>
list of identifiers and strings and Agda will return all the<br>
identifiers which:<br>
- are in scope in the current module<br>
- contain in their type *all* of the identifiers mentioned<br>
- contain as substring *all* of the mentioned strings<br>
<br>
For instance, using a fairly recent version of the stdlib,
from<br>
the module containing:<br>
<br>
==============================<wbr>=============<br>
open import Data.Nat<br>
open import Data.Nat.Properties</tt><br>
<tt><tt>==============================<wbr>=============</tt><br>
<br>
C-c C-z RET _+_ _*_ RET<br>
<br>
will return<br>
<br></tt>
<tt><tt>==============================<wbr>=============<br>
Definitions about _+_, _*_<br>
*-+-isCommutativeSemiring<br>
:
.Algebra.Structures.IsCommutat<wbr>iveSemiring<br>
.Agda.Builtin.Equality._≡_ _+_ _*_ 0 1<br>
*-cancelˡ-≡<br>
: {i j : ℕ}
(k : ℕ) →<br>
i + k * i .Agda.Builtin.Equality.≡ j + k * j →<br>
i .Agda.Builtin.Equality.≡ j<br>
*-distrib-+<br>
:
(.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOver _*_)<br>
_+_<br>
*-distribʳ-+<br>
:
(.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOverʳ _*_)<br>
_+_<br>
*-distribˡ-+<br>
:
(.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOverˡ _*_)<br>
_+_<br>
+-*-suc : (m n : ℕ) → m * suc n .Agda.Builtin.Equality.≡ m +
m * n<br>
^-distribˡ-+-*<br>
: (m n p :
ℕ) →<br>
(m ^ (n + p)) .Agda.Builtin.Equality.≡ (m ^ n) * (m ^ p)<br>
distribʳ-*-+<br>
:
(.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOverʳ _*_)<br>
_+_<br>
im≡jm+n⇒[i∸j]m≡n<br>
: (i j m n :
ℕ) →<br>
i * m .Agda.Builtin.Equality.≡ j * m + n →<br>
(i ∸ j) * m .Agda.Builtin.Equality.≡ n<br>
isCommutativeSemiring<br>
:
.Algebra.Structures.IsCommutat<wbr>iveSemiring<br>
.Agda.Builtin.Equality._≡_ _+_ _*_ 0 1<br></tt></tt>
<tt>==============================<wbr>=============<br>
<br>
and</tt> <tt><tt>C-c C-z RET _+_ _*_ "distr" RET</tt><br>
will filter definitions which are not about distributivity:<br>
<br></tt>
<tt><tt>==============================<wbr>=============<br></tt></tt>
<tt><tt>Definitions about _+_, _*_, "distr"<br>
*-distrib-+<br>
: (.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOver _*_)<br>
_+_<br>
*-distribʳ-+<br>
: (.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOverʳ _*_)<br>
_+_<br>
*-distribˡ-+<br>
: (.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOverˡ _*_)<br>
_+_<br>
^-distribˡ-+-*<br>
: (m n p : ℕ) →<br>
(m ^ (n + p)) .Agda.Builtin.Equality.≡ (m
^ n) * (m ^ p)<br>
distribʳ-*-+<br>
: (.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.Di<wbr>stributesOverʳ _*_)<br>
_+_<br>
==============================<wbr>=============</tt><br>
<br>
This search function respect the normalisation modifiers
(that<br>
is the (C-u)* you can type before most commands) and will
search<br>
types according to the normalisation level you've requested
(and<br>
print results accordingly).<br>
<br>
Cheers,<br>
--<br>
gallais<br>
<br>
<br></tt>
<div>
<div class="m_-2587342160859142376m_-7173118898084949436h5">
<div class="m_-2587342160859142376m_-7173118898084949436m_-296081957163068206moz-cite-prefix">On 15/02/18
16:52, Philip Wadler wrote:<br></div>
</div>
</div>
<blockquote type="cite">
<div>
<div class="m_-2587342160859142376m_-7173118898084949436h5">
<div dir="ltr">Is there anything like Hoogle for Agda? It would
save newbies like me a *lot* of time. Cheers, -- P<br>
<div>
<div><br></div>
<div>
<div class="m_-2587342160859142376m_-7173118898084949436m_-296081957163068206gmail_signature">
<div dir="ltr">
<div>
<div dir="ltr">. \ Philip Wadler, Professor of Theoretical
Computer Science,<br>
. /\ School of Informatics, University of
Edinburgh<br></div>
<div>. / \ and Senior Research Fellow, IOHK<br></div>
<div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div>
</div>
</div>
</div>
</div>
</div>
</div>
<br>
<fieldset class="m_-2587342160859142376m_-7173118898084949436m_-296081957163068206mimeAttachmentHeader">
</fieldset>
<br></div>
</div>
<pre>The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
</pre>
<br>
<fieldset class="m_-2587342160859142376m_-7173118898084949436m_-296081957163068206mimeAttachmentHeader">
</fieldset>
<br>
<pre>______________________________<wbr>_________________
Agda mailing list
<a class="m_-2587342160859142376m_-7173118898084949436m_-296081957163068206moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a class="m_-2587342160859142376m_-7173118898084949436m_-296081957163068206moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a>
</pre></blockquote>
<br></div>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote>
</div>
<br></div>
The University of Edinburgh is a charitable body, registered in
<br>Scotland, with registration number SC005336.
<br>______________________________<wbr>_________________
<br>Agda mailing list
<br><a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a>
<br></div></div></span></blockquote></div></div></div></div></blockquote></div><br></div></div></div>
</blockquote></div><br></div>