[Agda] Proposed minor additions to standard library

[Nils Anders Danielsson]

On 2010-09-14 11:43, Jason Reich wrote:
> I think that a Hoogle-like search engine would be fantastic. I've
> thought about trying to implement it myself but I'm not sure if I
> understand the particulars of the type system enough to give it a go.
>
> Do you think it should be any more complex than Haskell's Hoogle?

I don't know enough about Hoogle to answer this question. You have the
added complexity of dependent types, but on the other hand there are no
type classes.

A quick search indicates that David Delahaye has written a relevant
paper: Information Retrieval in a Coq Proof Library using Type
Isomorphisms (TYPES'99).

--
/NAD