Base-Library

Coq library for finite types, vectors, retracts, and inhabited types.

This library is based on the library for the lecture "Introduction to Computational Logics" at Saarland University.

Acknowledments

• Gert Smolka, Saarland University: wrote the initial version
• Sigurd Schneider
• Dominik Kirst
• Yannick Forster
• Fabian Kunze
• Maximilian Wuttke

Further contributions:

• Jan Christian Menz: contributed modules for finite types (See his Bachelor's Thesis "A Coq Library for Finite Types")
• Maximilian Wuttke: contributed modules for vectors, retracts, and inhabited types