Idris ou Agda

[Eduardo Ochs]

Oi lista,

alguém aqui sabe usar Idris ou Agda o suficiente pra formalizar
estruturas algébricas simples e provas sobre elas? E que toparia me
ajudar a formalizar umas coisas em Idris ou Agda, pra gente publicar
umas notas sobre essa formalização/tradução como coautores no Arxiv?
Acho que seriam pouquíssimos dias de trabalho... as coisas que eu mais
quero formalizar são essas aqui,

http://angg.twu.net/LATEX/2020J-ops-new.pdf#page=9
http://angg.twu.net/LATEX/2020favorite-conventions.pdf#page=17
http://angg.twu.net/LATEX/2020favorite-conventions.pdf#page=33
http://angg.twu.net/LATEX/2020favorite-conventions.pdf#page=35

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