Re: [isabelle] New AFP theory: List Index



Tobias Nipkow wrote:
> My immediate plea is for modular library components. Having those as
> top-level entries dramatically increases the likelyhood that they are
> reused.
>
> But you are quite right: Hackage offers some things worth emulating:
> - A listing of packages by category
> - cabal
> A complication is that Isabelle does not support hierarchical module
> names in the way Haskell (or Java or ...) does.
>   
A feature that I often miss, especially considering namespace pollution
problems. One of the top-candidates on my wish list
is something like import-qualified, giving the user control over what
symbols (and syntax) will be loaded into the toplevel-namespace.
Related to this would be the possibility to specify the public interface
of a theory. Currently, the hide-command allows one to hide
private symbols, but the other way round would be more comfortable.

Peter






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.