Commit 45c0c04b authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

renumerotation, suite

parent 3ca9a16d
......@@ -44,7 +44,7 @@ liste de lettres. Par exemple, le mot `MI` correspond ainsi à la liste
`[M;I]`, cette syntaxe étant un raccourci pour `M::I::nil`, lui même
correspondant à `cons M (cons I nil)`. Et la concaténation de
mots est ici la concaténation de listes `++` (nommée `app` en
Coq). Pour plus d'explications sur le type des listes, revoir le TD6.
Coq). Pour plus d'explications sur le type des listes, revoir le TD3.
Enfin, l'appartenance au langage `L` est modélisé en Coq
sous la forme du prédicat `lang : word->Prop`.
......
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