Cotoleta –Lean Library for Formalized Coding Theory–

This is the official website of cotoleta.
Cotoleta is a LEAN library for formalized coding theory
and stands for COding Theory Over the LEan Theorem-proof Assistant.

Formalized Objects:
-Repetition Codes
-Hamming Codes

Our library is available from the link below:
-lean 2: -= Cotoleta version 0.11 beta =-(2016/Sep/30)

Cotoleta for lean 3 is under development.
It will be coming soon. Stay tune.

-Formalization of Coding Theory using Lean,
Manabu Hagiwara, Kyosuke Nakano and Justin Kong,
ISITA2016, California, 2016.

Formalized by
-Manabu Hagiwara
-Justin Kong
-Kyosuke Nakano

Since 2016.