<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body 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>
===========================================<br>
open import Data.Nat<br>
open import Data.Nat.Properties</tt><br>
<tt><tt>===========================================</tt><br>
<br>
C-c C-z RET _+_ _*_ RET<br>
<br>
will return<br>
<br>
</tt><tt><tt>===========================================<br>
Definitions about _+_, _*_<br>
*-+-isCommutativeSemiring<br>
: .Algebra.Structures.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.DistributesOver _*_)<br>
_+_<br>
*-distribʳ-+<br>
: (.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.DistributesOverʳ _*_)<br>
_+_<br>
*-distribˡ-+<br>
: (.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.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.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.IsCommutativeSemiring<br>
.Agda.Builtin.Equality._≡_ _+_ _*_ 0 1<br>
</tt></tt><tt>===========================================<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>===========================================<br>
</tt></tt><tt><tt>Definitions about _+_, _*_, "distr"<br>
*-distrib-+<br>
: (.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.DistributesOver _*_)<br>
_+_<br>
*-distribʳ-+<br>
: (.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.DistributesOverʳ _*_)<br>
_+_<br>
*-distribˡ-+<br>
: (.Agda.Builtin.Equality._≡_<br>
.Algebra.FunctionProperties.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.DistributesOverʳ _*_)<br>
_+_<br>
===========================================</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><tt><tt></tt></tt>
<div class="moz-cite-prefix">On 15/02/18 16:52, Philip Wadler wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAESRbcqn3Lmi4Bmwx9fybKFq+rFDsfLks9ba+SAGHtrDdrj=5Q@mail.gmail.com">
<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="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" moz-do-not-send="true">http://homepages.inf.ed.ac.uk/wadler/</a></span></div>
</div>
</div>
</div>
</div>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>