diff options
-rw-r--r-- | dev/TODO | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/dev/TODO b/dev/TODO new file mode 100644 index 000000000..a7996b373 --- /dev/null +++ b/dev/TODO @@ -0,0 +1,14 @@ + + o Himsg + en faire un foncteur qui prend en arguments des fonctions + sachant afficher les termes, et retournant des fonctions + expliquant les messages d'erreur (de typage, d'inductifs, de + convertibilité), retournant des std_ppcmds. + + o Lexer + à compléter + + o Toplevel + - boucle principale, affichage des erreur, du prompt + - parsing de la ligne de commande (Arg ?) + |