Coq

Usamos o proof assistant Coq para algumas atividades.

• Instale o Coq, seguindo as instruções no seu site.
• Crie uma pasta no teu sistema chamada fmc1-coq e bote no GitHub (que?!?).
• Crie uma pasta no teu sistema chamada lf e bote no GitHub também.
• Baixe o arquivo .tgz que tenho no pub/. Esse arquivo é o livro [SF1].
• Abra o arquivo dentro da pasta lf, assim tu vai ter o livro inteiro nessa pasta. Caso que acabou criando uma lf dentro da lf, resolva, não precisamos disso.
• Crie um .gitignore tanto na lf quanto na fmc1-coq (exemplo no pub/ também, que é o padrão do github para Coq).
• Cada vez que você trabalha em qualquer arquivo em qualquer pasta, não esqueça de commit’ar teu trabalho imediatamente, mesmo sendo um progresso pequeno; e faça push imediatamente: é teu “comprovante” que tal dia fez tal trabalho!

Como posso compartilhar meu código para receber feedback ou tirar uma dúvida?

• Para mostrar teu código com o resto da turma no Slack use o CollaCoq e compartilhe o link; alternativamente podes compartilhar teu repo no github (que já deve ser visível no teu profile no Zulip!)