3 ms·
Sure, why not. It seems to be a pretty good exposition of the material. When I got interested in this stuff many years ago I worked my way through the 'typing r
by cjfd 1y ago
Sure, why not. It seems to be a pretty good exposition of the material. When I got interested in this stuff many years ago I worked my way through the 'typing rules' in the coq (nowadays rocq) manual. That is a 'slightly' higher friction way of learning this stuff. This document seems to be more pedagogical.
- avodonosov 1y agoHave you found this stuff useful during the many years since you learned it? Or you don't mean you mastered it enough to judge its usefulness?
- cjfd 1y agoI have a personal coq/rocq project regarding the verification of software so for that purpose it is highly useful. I also wrote a proof assistent myself (https://github.com/chrisd1977/system https://github.com/chrisd1977/system).