main.agda

[jcguu95]

Hello! I find your book very helpful! Thank you very much for your work!

I think it's going to help people who don't know computer well to add a main.agda. It should import all the agda codes, and compile while all proofs are correct. Anyone then can follow a short instruction to witness this by themselves. They can also change the proof a bit, and witness the failure.