Différences

Ci-dessous, les différences entre deux révisions de la page.

--- lang:rocq [2025/09/17 14:49] – Ajout des exemples de Coq'Art root
+++ lang:rocq [2025/09/18 16:28] (Version actuelle) – Ajout de "Définition inductive" avec exemple root
@@ Ligne 1: / Ligne 1: @@
 [[https://rocq-prover.org|Site web]]
+=====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 :: l'' avec ''%%m <= n%%'' alors ''m :: n :: l'' est ordonnée.
+<code ocaml>
+Inductive sorted : list Z -> Prop :=
+  | sorted0 : sorted nil
+  | sorted1 : forall z:Z, sorted (z :: nil)
+  | sorted2 :
+      forall (z1 z2:Z) (l:list Z),
+        z1 <= z2 ->
+        sorted (z2 :: l) -> sorted (z1 :: z2 :: l).
+</code>
 =====Documentation=====