tchajed/coq-classes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
A library of typeclasses for Coq
44 commits 2 branches 0 tags 94 KiB
  • Rocq Prover 92.6%
  • Makefile 7.4%
Find a file
Exact
Tej Chajed c4086f8ca7
 Merge pull request #2 from tchajed/fix-deprecations 
Fix deprecation warnings and update CI
2026-04-01 07:52:02 -05:00
.github/workflows Use rocq compile, coq_version CI, fix permissions 2026-04-01 07:49:09 -05:00
src Fix deprecation warnings and update CI 2026-04-01 07:41:02 -05:00
.gitignore Add _RocqProject to .gitignore 2026-04-01 07:49:46 -05:00
_RocqProject Fix deprecation warnings and update CI 2026-04-01 07:41:02 -05:00
libname Rename library 2018-11-13 07:15:25 -05:00
LICENSE Add license 2021-05-31 10:16:44 -04:00
Makefile Use rocq compile, coq_version CI, fix permissions 2026-04-01 07:49:09 -05:00
README.md Fix README badge 2021-05-31 09:57:49 -04:00

README.md

A few Coq typeclasses

CI

Includes the following typeclasses, as well as several instances for standard datatypes:

  • EqualDec for decidable equality
  • Default 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.

Installation

git submodule add https://github.com/tchajed/coq-classes vendor/classes