[Agda] Proposed minor additions to standard library

[Jason Reich]

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?

Jason

Nils Anders Danielsson wrote:
> On 2010-09-14 06:12, Gregory Crosswhite wrote:
>>      1) Adding a function mapDec to Relation.Nullary that allows users
>>         to change between types Dec A to Dec B given maps (A -> B) and
>>         (B -> A).
> 
> import Relation.Nullary.Decidable as Dec
> 
> ...Dec.map...Dec.map′...
> 
> It would be good to have a Hoogle-like search engine for Agda. Is anyone
> interested in implementing one?
> 
>>      2) Creating a module for ExpFunctors -- that is, invariant
>>         functors which can take you between F A to F B if you have
>>         maps (A -> B) and (B -> A).
> 
> Is ExpFunctor an established name? It seems as if this construction
> should be a special case of something else.
> 
> I am a bit reluctant to add this module unless you have more use cases
> for it.
> 
> -- 
> /NAD
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda