Double flèche vers le bas en LaTeX (\Downarrow)

Où il est utilisé

Trace une flèche à double trait vers le bas, utilisée pour l’évaluation à grands pas en sémantique des langages de programmation.

La sémantique opérationnelle écrit e \Downarrow v pour signifier que l’expression e s’évalue en la valeur v dans le style à grands pas, principal usage technique de ce symbole. Dans les diagrammes et les démonstrations logiques, elle peut marquer une étape d’inférence verticale. Comme les autres flèches verticales, \Downarrow est un délimiteur : \Big\Downarrow en donne une version plus haute. Ne la confondez pas avec \downarrow, qui dans la même sémantique peut signifier la terminaison. Définissez votre convention en introduisant le jugement. La sémantique à petits pas utilise au contraire \to ou \longrightarrow pour les étapes de réduction uniques, et \to^* pour leur clôture réflexive et transitive.

Exemple minimal compilable

Collez-le dans un fichier .tex vide et compilez avec pdfLaTeX, XeLaTeX ou LuaLaTeX.

\documentclass{article}
\begin{document}
Down Arrow (Double): $\Downarrow$

\[ \frac{e_1 \Downarrow v_1 \quad e_2 \Downarrow v_2}{e_1 + e_2 \Downarrow v} \]
\end{document}

Symboles associés

• Flèche gauche-droite\leftrightarrow
• Longue double flèche vers la droite\Longrightarrow
• Longue flèche gauche-droite\longleftrightarrow
• Longue double flèche vers la gauche\Longleftarrow
• Flèche haut-bas\updownarrow
• Double flèche vers le haut\Uparrow

Questions fréquentes

Comment écrire Double flèche vers le bas en LaTeX ?

Tapez \Downarrow en mode mathématique, par exemple $\frac{e_1 \Downarrow v_1 \quad e_2 \Downarrow v_2}{e_1 + e_2 \Downarrow v}$. La commande fonctionne en LaTeX standard sans charger de paquet.

Quel paquet faut-il pour \Downarrow ?

Aucun. \Downarrow fait partie de LaTeX standard : le préambule n’a besoin que de la classe de document.

Peut-on utiliser \Downarrow en mode texte, ou seulement en mode mathématique ?

Seulement en mode mathématique. Hors de $...$, LaTeX s’arrête avec "Missing $ inserted" : dans le texte, écrivez $\Downarrow$. Si vous voulez seulement le glyphe dans le texte, collez le caractère Unicode ⇓ (avec XeLaTeX ou LuaLaTeX et une police qui le contient).