some simple&naive formal proof of trivial Number Theory, using Agda/Coq
just to practice skills (aka a project of Just A Toy (JAT) )
The first choice is Coq, because I cannot remember shortcuts in emacs, which is 钦定-ed by Agda used in interactive mode. (Who is Atom?)
But with a little try, I found I do not know anything about Coq.
So It is an Agda project. (Does agda have any module manager?)
- Agda 2.6
- Agda-stdlib 0.16