lang:rocq
Ceci est une ancienne révision du document !
Table des matières
Définitions
Définition inductive
C'est quand on part d'un cas particulier pour aller vers un cas général.
Exemple :
- Une liste vide est ordonnée.
- Une liste avec une valeur est ordonnée.
- Une liste de type
n :: lavecm <= nalorsm :: n :: lest ordonnée.
Documentation
Université de Pennsylvanie Archive Logical Foundations v9.0.0 Programming Language Foundations v9.0.0 Verified Functional Algorithms v9.0.0 QuickChick: Property-Based Testing in Coq v9.0.0 Verifiable C v8.16 Separation Logic Foundations v9.0.0
Exemples
lang/rocq.1758205435.txt.gz · Dernière modification : de root