[Agda] Hoogle for Agda?

[Philip Wadler]

Thanks!

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?

Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On 15 February 2018 at 14:01, Guillaume Allais <
guillaume.allais at ens-lyon.org> wrote:

> Hi Phil,
>
> There's a *very basic* search functionality which you can invoke
> from emacs using C-c C-z. You can then input a space-separated
> list of identifiers and strings and Agda will return all the
> identifiers which:
> - are in scope in the current module
> - contain in their type *all* of the identifiers mentioned
> - contain as substring *all* of the mentioned strings
>
> For instance, using a fairly recent version of the stdlib, from
> the module containing:
>
> ===========================================
> open import Data.Nat
> open import Data.Nat.Properties
> ===========================================
>
> C-c C-z RET _+_ _*_ RET
>
> will return
>
> ===========================================
> Definitions about _+_, _*_
>   *-+-isCommutativeSemiring
>           : .Algebra.Structures.IsCommutativeSemiring
>             .Agda.Builtin.Equality._≡_ _+_ _*_ 0 1
>   *-cancelˡ-≡
>           : {i j : ℕ} (k : ℕ) →
>             i + k * i .Agda.Builtin.Equality.≡ j + k * j →
>             i .Agda.Builtin.Equality.≡ j
>   *-distrib-+
>           : (.Agda.Builtin.Equality._≡_
>              .Algebra.FunctionProperties.DistributesOver _*_)
>             _+_
>   *-distribʳ-+
>           : (.Agda.Builtin.Equality._≡_
>              .Algebra.FunctionProperties.DistributesOverʳ _*_)
>             _+_
>   *-distribˡ-+
>           : (.Agda.Builtin.Equality._≡_
>              .Algebra.FunctionProperties.DistributesOverˡ _*_)
>             _+_
>   +-*-suc : (m n : ℕ) → m * suc n .Agda.Builtin.Equality.≡ m + m * n
>   ^-distribˡ-+-*
>           : (m n p : ℕ) →
>             (m ^ (n + p)) .Agda.Builtin.Equality.≡ (m ^ n) * (m ^ p)
>   distribʳ-*-+
>           : (.Agda.Builtin.Equality._≡_
>              .Algebra.FunctionProperties.DistributesOverʳ _*_)
>             _+_
>   im≡jm+n⇒[i∸j]m≡n
>           : (i j m n : ℕ) →
>             i * m .Agda.Builtin.Equality.≡ j * m + n →
>             (i ∸ j) * m .Agda.Builtin.Equality.≡ n
>   isCommutativeSemiring
>           : .Algebra.Structures.IsCommutativeSemiring
>             .Agda.Builtin.Equality._≡_ _+_ _*_ 0 1
> ===========================================
>
> and C-c C-z RET _+_ _*_ "distr" RET
> will filter definitions which are not about distributivity:
>
> ===========================================
> Definitions about _+_, _*_, "distr"
>   *-distrib-+
>    : (.Agda.Builtin.Equality._≡_
>       .Algebra.FunctionProperties.DistributesOver _*_)
>      _+_
>   *-distribʳ-+
>    : (.Agda.Builtin.Equality._≡_
>       .Algebra.FunctionProperties.DistributesOverʳ _*_)
>      _+_
>   *-distribˡ-+
>    : (.Agda.Builtin.Equality._≡_
>       .Algebra.FunctionProperties.DistributesOverˡ _*_)
>      _+_
>   ^-distribˡ-+-*
>    : (m n p : ℕ) →
>      (m ^ (n + p)) .Agda.Builtin.Equality.≡ (m ^ n) * (m ^ p)
>   distribʳ-*-+
>    : (.Agda.Builtin.Equality._≡_
>       .Algebra.FunctionProperties.DistributesOverʳ _*_)
>      _+_
> ===========================================
>
> This search function respect the normalisation modifiers (that
> is the (C-u)* you can type before most commands) and will search
> types according to the normalisation level you've requested (and
> print results accordingly).
>
> Cheers,
> --
> gallais
>
>
> On 15/02/18 16:52, Philip Wadler wrote:
>
> Is there anything like Hoogle for Agda? It would save newbies like me a
> *lot* of time. Cheers, -- P
>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
>
> _______________________________________________
> Agda mailing listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180215/c1994621/attachment-0001.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180215/c1994621/attachment-0001.ksh>