@@ -265,7 +265,7 @@ Laissons de côté les preuves pour l'instant. Pour pouvoir prouver des programm
Ce langage est très proche d'OCaml, mais il y a quelques différences. Par exemple, les fonctions sont définies avec `Definition` au lieu de `let`, les définitions récursives avec `Fixpoint` au lieu de `let rec` et les types sont définis avec `Inductive` au lieu de `type`. Il n'y a pas de restrictions sur les noms des constructeurs et les noms de variables, qui peuvent commencer aussi bien par une minuscule qu'une majuscule.
Mais la plus grande différence, à la fois avec OCaml et avec les autres langages de programmation que vous connaissez, est que Gallina n'est pas un langage "Turing-complet". Pour pouvoir définir une fonction en Gallina, il faut pouvoir prouver qu'elle termine. Le plus souvent, cela se fait en utilisant la récursion structurelle, ce qui veut dire que la fonction à un argument qui diminue (structurellement) à chaque appel récursif. Nous définirons des fonctions récursives structurelles dans la suite de ce TP. Mais commençons par quelques exemples de fonctions non récursives.
Mais la plus grande différence, à la fois avec OCaml et avec les autres langages de programmation que vous connaissez, est que Gallina n'est pas un langage "Turing-complet". Pour pouvoir définir une fonction en Gallina, il faut pouvoir prouver qu'elle termine. Le plus souvent, cela se fait en utilisant la récursion structurelle, ce qui veut dire que la fonction a un argument qui diminue (structurellement) à chaque appel récursif. Nous définirons des fonctions récursives structurelles dans la suite de ce TP. Mais commençons par quelques exemples de fonctions non récursives.
