3 ms·
I worked with Adam one summer before he had that coq textbook, he’s definitely a wizard of proof automation in coq. I only much more recently learned how ltac
by carterschonwald 9y ago
I worked with Adam one summer before he had that coq textbook, he’s definitely a wizard of proof automation in coq. I only much more recently learned how ltac case expressions also backtrack!
- kmill 9y agoFor the benefit of people without specific knowledge of people at MIT: Adam is Adam Chlipala http://adam.chlipala.net/ http://adam.chlipala.net/