Da' pra typesettear arvores de deducao com Dednat6 no Overleaf

[Eduardo Ochs]

Oi lista,

há poucos dias atrás eu descobri que um monte de gente no Zulip Chat
de Applied Category Theory usa Overleaf, que eu não fazia idéia de que
poderia ser usado pra papers complicados com montes de diagramas em
Tikz...

...aí ontem de noite eu fui ver se o Dednat6 funcionava em Overleaf, e
ele funcionou direto - basta fazer isso aqui:

1. Download [dednat6-minimal.zip]
2. Import the .zip
3. [Change the compiler] to lualatex
4. Click on "Recompile". You should get a PDF like [this].
5. Take a look at these [slides] and at the [TUGBoat article]
6. Make small changes to demo-minimal.tex, recompile, rinse, repeat

A versão com links dessas instruções está aqui:

http://angg.twu.net/dednat6.html#quick-start

Pra mim o Dednat6 é utilíssimo pra typesettear árvores de dedução
grandes, porque eu posso editá-las em ASCII art - tem três exemplos
pequenos aqui:

http://angg.twu.net/dednat6/demo-minimal.tex.html
http://angg.twu.net/dednat6/demo-minimal.pdf

Acho que 99% dos lógicos não têm problema nenhum pra typesettear
árvores grandes - de, digamos, mais de 15 nodes - usando só proof.sty
ou bussproofs, mas pra mim era quase impossível... talvez tenha outras
pessoas como eu aqui, pras quais o Dednat6 possa ser útil.

Se alguém quiser testar o Dednat6 no Overleaf ou fora do Overleaf,
seja por achar que vai ser útil ou só por curiosidade, eu agradeço
horrores. Por enquanto o Dednat6 só tem um usuário não-anônimo além de
mim, o Fernando Lucatelli Nunes - e ele 1) não usa Overleaf e 2) usa
só a parte do Dednat6 que gera diagramas pra Categorias, não a parte
de árvores.

[[]],
Eduardo Ochs
http://angg.twu.net/math-b.html