Ltac est un bousin sans nom qui est la source d'un tas de problèmes, le genre de code qu'il suffit de regarder fixement pour faire péter un développement à l'autre bout de la planète.
Justement, au sujet de Ltac, vous avez des idées ou des pistes pour l'améliorer et faciliter l'écriture de tactiques ? Si on prend l'exemple de patrick_g :
Par exemple dans de nombreux articles de géométrie arithmétique ou de géométrie algébrique on peut voir des phrases du style : "Par un argument à la GAGA il est facile de voir que blabla".
il doit bien être possible d'écrire une tactique gaga, mais ce possible reste souvent « théorique », écrire une tactique finissant par rendre à moitié fou (j'ai jamais bien compris comment marchait le système).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Perl6
Posté par kantien . En réponse au journal La recherche en langages de programmation au quotidien. Évalué à 2. Dernière modification le 09 février 2018 à 21:26.
Justement, au sujet de Ltac, vous avez des idées ou des pistes pour l'améliorer et faciliter l'écriture de tactiques ? Si on prend l'exemple de patrick_g :
il doit bien être possible d'écrire une tactique
gaga, mais ce possible reste souvent « théorique », écrire une tactique finissant par rendre à moitié fou (j'ai jamais bien compris comment marchait le système).Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.