Commit 5ac8bfba authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

typo

parent 83f91110
......@@ -89,7 +89,7 @@ Réduction d'un match : lorsque la tête d'un match commençe par un constructeu
## Fix
La construction ̀Fixpoint` va permettre de créer des fonctions récursives en Coq. Attention, comme mentionné auparavant, certaines fonctions récursives seront rejetées par Coq, qui ne va accepter que des *fonctions récursives structurellement décroissantes*.
La construction `Fixpoint` va permettre de créer des fonctions récursives en Coq. Attention, comme mentionné auparavant, certaines fonctions récursives seront rejetées par Coq, qui ne va accepter que des *fonctions récursives structurellement décroissantes*.
Le mot-clé `Fixpoint` s'emploie à la place du mot-clé `Definition`, voir les exemples plus bas (ou dans les TD).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment