Séance de cours
Coq: Vue d'ensemble
Description
Cette séance de cours introduit Coq, un assistant de preuve, se concentrant sur le théorème et le_comm, qui indique que pour toutes les propositions P et Q, si P et Q sont vraies, alors Q et P sont également vraies. La séance de cours couvre le processus de prouver ce théorème étape par étape à l'aide de l'assistant de preuve de Coq.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.