Définition de la classe de réécriture à intégrer
Résumé
Nous définissons les objets qui doivent être rajoutés à Coq pour pouvoir définir des fonctions à l'aide de règles de récriture, et décrivons les conditions qui doivent être vérifiées pour que la correction de Coq soit préservée. Cela constitue une sorte de ``cahier des charges'' pour le futur prototype.