<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="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 14:01, Guillaume Allais <span dir="ltr"><<a href="mailto:guillaume.allais@ens-lyon.org" target="_blank">guillaume.allais@ens-lyon.org</a>></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.<wbr>IsCommutativeSemiring<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.<wbr>DistributesOver _*_)<br>
                    _+_<br>
          *-distribʳ-+<br>
                  : (.Agda.Builtin.Equality._≡_<br>
                     .Algebra.FunctionProperties.<wbr>DistributesOverʳ _*_)<br>
                    _+_<br>
          *-distribˡ-+<br>
                  : (.Agda.Builtin.Equality._≡_<br>
                     .Algebra.FunctionProperties.<wbr>DistributesOverˡ _*_)<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.<wbr>DistributesOverʳ _*_)<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.<wbr>IsCommutativeSemiring<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.<wbr>DistributesOver _*_)<br>
             _+_<br>
          *-distribʳ-+<br>
           : (.Agda.Builtin.Equality._≡_<br>
              .Algebra.FunctionProperties.<wbr>DistributesOverʳ _*_)<br>
             _+_<br>
          *-distribˡ-+<br>
           : (.Agda.Builtin.Equality._≡_<br>
              .Algebra.FunctionProperties.<wbr>DistributesOverˡ _*_)<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.<wbr>DistributesOverʳ _*_)<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="h5"><tt><tt></tt></tt>
    <div class="m_-296081957163068206moz-cite-prefix">On 15/02/18 16:52, Philip Wadler wrote:<br>
    </div>
    </div></div><blockquote type="cite"><div><div class="h5">
      <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_-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_-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_-296081957163068206mimeAttachmentHeader"></fieldset>
      <br>
      <pre>______________________________<wbr>_________________
Agda mailing list
<a class="m_-296081957163068206moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a class="m_-296081957163068206moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <br>
  </div>

<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>