Other "standard" libraries

"Standard" Libraries for other Languages

• Agda https://github.com/agda/agda-stdlib
• F* https://github.com/FStarLang/FStar/tree/master/ulib
• Idris https://github.com/idris-lang/Idris-dev/tree/master/libs
• Lean https://github.com/leanprover/mathlib

Other "Standard" Libraries for Coq

There is a cottage industry of alternative standard libraries/extensions to the standard library.

• coq-ext-lib
  • Type classes
  • Originally minimal use of dependent types (that has changed a little bit).
  • Separation between definitions and proofs, e.g. Monad and MonadLaws.
  • Disciplined use of notations to avoid trivial import problems with libraries that are compatible except for notations.
  • Universe polymorphism and primitive projections everywhere.
  • Module naming convention ExtLib.Data.Nat, ExtLib.Structures.Monad, etc. Generally CamelCase for types and snake_case for definitions.
  • License: MIT
• coq-haskell
  • Type classes
  • Mostly for smoothing the extraction from Coq to Haskell.
  • Module naming convention Hask.Data.List, names reflect their Haskell names, e.g. Maybe instead of option.
• coq-prelude
  • "Inspired by Haskell"
  • Mostly focused on Monads
  • Module naming convention Control.Classes, Control.State, etc.
  • camelCase for definitions and CamelCase for types/classes.
  • License: GPL3
• mathclasses
  • Type classes
  • Pervasive setoids
  • License: Public domain
• ssreflect
  • Canonical structures
• stdpp
  • Type classes
  • Mostly data types, not a lot of generic interfaces.
  • Lots of hints and patterns to improve type class resolution and type checking.
  • Module naming convention: stdpp.fin, snake_case for identifiers