Roadmap

The roadmap for things to come.

Future

• Universe polymorphic versions of the core data types, e.g. list, option, pair, etc.
• Functorized versions of the core data types that can be used in cases where fresh universes are necessary but you don't want to use universe polymorphic versions.
• Speculative: the type class is meant to provide a setoid interface to every type. It needs some work though.

Current Development

• At the moment, this library is growing organically from the development of the mirror-core library.

Version 0.2

• Re-organization of the library structure
  • Structures contains interfaces
  • Data contains implementations
  • Tactics contains tactics for generic reasoning.
  • Programming contains type classes for "standard/natural" uses of data types
    • These are all defined on top of the core library so that they do not have to be used to make use of the core library.

Version 0.0

• Pretty much unstructured commits and combining several previous projects
• The structure to the library is to separate reasoning and computation (this is for the sake of computational efficiency).
  • Type classes are used to connect implementations and reasoning principles.
• Components
  • Facilities for nicer reasoning about boolean functions.
  • Sketch of a library of Monads
    • This includes reasoning principles.
  • Sketch of some collections, (finite) maps, (finite) sets, graphs