Seta dupla para baixo em LaTeX (\Downarrow)

Onde é usado

Desenha uma seta de haste dupla para baixo, usada para a avaliação de passo grande na semântica de linguagens de programação.

A semântica operacional escreve e \Downarrow v para dizer que a expressão e é avaliada para o valor v no estilo de passo grande, o principal uso técnico desse símbolo. Em diagramas e demonstrações lógicas, pode marcar um passo de inferência vertical. Como as demais setas verticais, \Downarrow é um delimitador, então \Big\Downarrow produz uma versão mais alta. Não a confunda com \downarrow, que na mesma semântica pode significar terminação. Defina sua convenção ao introduzir o julgamento. A semântica de passo pequeno, por outro lado, usa \to ou \longrightarrow para passos de redução únicos, e \to^* para o seu fecho reflexivo e transitivo.

Exemplo mínimo compilável

Cole isto em um arquivo .tex vazio e compile com 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}

Símbolos relacionados

• Seta para a esquerda e para a direita\leftrightarrow
• Seta longa dupla para a direita\Longrightarrow
• Seta longa para a esquerda e para a direita\longleftrightarrow
• Seta longa dupla para a esquerda\Longleftarrow
• Seta para cima e para baixo\updownarrow
• Seta dupla para cima\Uparrow

Perguntas frequentes

Como escrever Seta dupla para baixo em LaTeX?

Digite \Downarrow no modo matemático, por exemplo $\frac{e_1 \Downarrow v_1 \quad e_2 \Downarrow v_2}{e_1 + e_2 \Downarrow v}$. Funciona no LaTeX padrão sem carregar nenhum pacote.

Qual pacote é necessário para \Downarrow?

Nenhum. \Downarrow faz parte do LaTeX padrão, então compila só com a classe do documento no preâmbulo.

Posso usar \Downarrow no modo texto ou só no modo matemático?

Só no modo matemático. Fora de $...$ o LaTeX para com "Missing $ inserted", então no texto escreva $\Downarrow$. Se você só precisa do glifo no texto, cole o caractere Unicode ⇓ (com XeLaTeX ou LuaLaTeX e uma fonte que o tenha).