Différences

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

--- lang:rocq [2025/09/18 16:23] – Ajout de "Définition inductive" root
+++ lang:rocq [2025/09/18 16:28] (Version actuelle) – Ajout de "Définition inductive" avec exemple root
@@ Ligne 12: / Ligne 12: @@
   * 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=====