A library of typeclasses for Coq
Includes the following typeclasses, as well as several instances for standard datatypes:
EqualDec
for decidable equalityDefault
for inhabited types, with witness default
.Ordering
for totally ordered types, which includes instances for list
and string
.This dependency is mainly so multiple projects share the same typeclass definitions.
git submodule add https://github.com/tchajed/coq-classes vendor/classes