Linear Error-correcting Codes in Coq

Contents moved to this page.